:: BVFUNC_9 semantic presentation

E1: for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 '&' b3 '<' b2
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
let c4 be Element of c1; :: according to BVFUNC_1:def 15
assume (c2 '&' c3) . c4 = TRUE ;
then (c2 . c4) '&' (c3 . c4) = TRUE by VALUAT_1:def 6;
hence c2 . c4 = TRUE by MARGREL1:45;
end;

E2: for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( (b2 '&' b3) '&' b4 '<' b2 & (b2 '&' b3) '&' b4 '<' b3 )
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E3: (c2 '&' c3) '&' c4 = (c4 '&' c3) '&' c2 by BVFUNC_1:7;
((c4 '&' c3) '&' c2) 'imp' c2 = I_el c1 by BVFUNC_6:39;
hence (c2 '&' c3) '&' c4 '<' c2 by E3, BVFUNC_1:19;
E4: (c2 '&' c3) '&' c4 = (c2 '&' c4) '&' c3 by BVFUNC_1:7;
((c2 '&' c4) '&' c3) 'imp' c3 = I_el c1 by BVFUNC_6:39;
hence (c2 '&' c3) '&' c4 '<' c3 by E4, BVFUNC_1:19;
end;

E3: for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN holds
( ((b2 '&' b3) '&' b4) '&' b5 '<' b2 & ((b2 '&' b3) '&' b4) '&' b5 '<' b3 )
proof
let c1 be non empty set ;
let c2, c3, c4, c5 be Element of Funcs c1,BOOLEAN ;
thus ((c2 '&' c3) '&' c4) '&' c5 '<' c2
proof
E4: ((c2 '&' c3) '&' c4) '&' c5 = (c5 '&' c4) '&' (c3 '&' c2) by BVFUNC_1:7
.= ((c5 '&' c4) '&' c3) '&' c2 by BVFUNC_1:7 ;
(((c5 '&' c4) '&' c3) '&' c2) 'imp' c2 = I_el c1 by BVFUNC_6:39;
hence ((c2 '&' c3) '&' c4) '&' c5 '<' c2 by E4, BVFUNC_1:19;
end;
E4: ((c2 '&' c3) '&' c4) '&' c5 = ((c2 '&' c4) '&' c3) '&' c5 by BVFUNC_1:7
.= ((c2 '&' c4) '&' c5) '&' c3 by BVFUNC_1:7 ;
(((c2 '&' c4) '&' c5) '&' c3) 'imp' c3 = I_el c1 by BVFUNC_6:39;
hence ((c2 '&' c3) '&' c4) '&' c5 '<' c3 by E4, BVFUNC_1:19;
end;

E4: for b1 being non empty set
for b2, b3, b4, b5, b6 being Element of Funcs b1,BOOLEAN holds
( (((b2 '&' b3) '&' b4) '&' b5) '&' b6 '<' b2 & (((b2 '&' b3) '&' b4) '&' b5) '&' b6 '<' b3 )
proof
let c1 be non empty set ;
let c2, c3, c4, c5, c6 be Element of Funcs c1,BOOLEAN ;
thus (((c2 '&' c3) '&' c4) '&' c5) '&' c6 '<' c2
proof
E5: (((c2 '&' c3) '&' c4) '&' c5) '&' c6 = (c6 '&' c5) '&' (c4 '&' (c3 '&' c2)) by BVFUNC_1:7
.= ((c6 '&' c5) '&' c4) '&' (c3 '&' c2) by BVFUNC_1:7
.= (((c6 '&' c5) '&' c4) '&' c3) '&' c2 by BVFUNC_1:7 ;
((((c6 '&' c5) '&' c4) '&' c3) '&' c2) 'imp' c2 = I_el c1 by BVFUNC_6:39;
hence (((c2 '&' c3) '&' c4) '&' c5) '&' c6 '<' c2 by E5, BVFUNC_1:19;
end;
E5: (((c2 '&' c3) '&' c4) '&' c5) '&' c6 = (((c2 '&' c4) '&' c3) '&' c5) '&' c6 by BVFUNC_1:7
.= (((c2 '&' c4) '&' c5) '&' c3) '&' c6 by BVFUNC_1:7
.= (((c2 '&' c4) '&' c5) '&' c6) '&' c3 by BVFUNC_1:7 ;
((((c2 '&' c4) '&' c5) '&' c6) '&' c3) 'imp' c3 = I_el c1 by BVFUNC_6:39;
hence (((c2 '&' c3) '&' c4) '&' c5) '&' c6 '<' c3 by E5, BVFUNC_1:19;
end;

E5: for b1 being non empty set
for b2, b3, b4, b5, b6, b7 being Element of Funcs b1,BOOLEAN holds
( ((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7 '<' b2 & ((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7 '<' b3 )
proof
let c1 be non empty set ;
let c2, c3, c4, c5, c6, c7 be Element of Funcs c1,BOOLEAN ;
thus ((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7 '<' c2
proof
E6: ((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7 = (c7 '&' c6) '&' (c5 '&' (c4 '&' (c3 '&' c2))) by BVFUNC_1:7
.= ((c7 '&' c6) '&' c5) '&' (c4 '&' (c3 '&' c2)) by BVFUNC_1:7
.= (((c7 '&' c6) '&' c5) '&' c4) '&' (c3 '&' c2) by BVFUNC_1:7
.= ((((c7 '&' c6) '&' c5) '&' c4) '&' c3) '&' c2 by BVFUNC_1:7 ;
(((((c7 '&' c6) '&' c5) '&' c4) '&' c3) '&' c2) 'imp' c2 = I_el c1 by BVFUNC_6:39;
hence ((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7 '<' c2 by E6, BVFUNC_1:19;
end;
E6: ((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7 = (c7 '&' c6) '&' (c5 '&' (c4 '&' (c3 '&' c2))) by BVFUNC_1:7
.= ((c7 '&' c6) '&' c5) '&' (c4 '&' (c3 '&' c2)) by BVFUNC_1:7
.= (((c7 '&' c6) '&' c5) '&' c4) '&' (c3 '&' c2) by BVFUNC_1:7
.= ((((c7 '&' c6) '&' c5) '&' c4) '&' c2) '&' c3 by BVFUNC_1:7 ;
(((((c7 '&' c6) '&' c5) '&' c4) '&' c2) '&' c3) 'imp' c3 = I_el c1 by BVFUNC_6:39;
hence ((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7 '<' c3 by E6, BVFUNC_1:19;
end;

E6: for b1 being non empty set
for b2, b3, b4, b5, b6, b7, b8 being Element of Funcs b1,BOOLEAN holds
( (((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8 '<' b2 & (((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8 '<' b3 )
proof
let c1 be non empty set ;
let c2, c3, c4, c5, c6, c7, c8 be Element of Funcs c1,BOOLEAN ;
thus (((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 '<' c2
proof
E7: (((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 = (c8 '&' c7) '&' (c6 '&' (c5 '&' (c4 '&' (c3 '&' c2)))) by BVFUNC_1:7
.= ((c8 '&' c7) '&' c6) '&' (c5 '&' (c4 '&' (c3 '&' c2))) by BVFUNC_1:7
.= (((c8 '&' c7) '&' c6) '&' c5) '&' (c4 '&' (c3 '&' c2)) by BVFUNC_1:7
.= ((((c8 '&' c7) '&' c6) '&' c5) '&' c4) '&' (c3 '&' c2) by BVFUNC_1:7
.= (((((c8 '&' c7) '&' c6) '&' c5) '&' c4) '&' c3) '&' c2 by BVFUNC_1:7 ;
((((((c8 '&' c7) '&' c6) '&' c5) '&' c4) '&' c3) '&' c2) 'imp' c2 = I_el c1 by BVFUNC_6:39;
hence (((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 '<' c2 by E7, BVFUNC_1:19;
end;
E7: (((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 = ((((c2 '&' (c4 '&' c3)) '&' c5) '&' c6) '&' c7) '&' c8 by BVFUNC_1:7
.= (((c2 '&' (c5 '&' (c4 '&' c3))) '&' c6) '&' c7) '&' c8 by BVFUNC_1:7
.= ((c2 '&' (c6 '&' (c5 '&' (c4 '&' c3)))) '&' c7) '&' c8 by BVFUNC_1:7
.= (c2 '&' (c7 '&' (c6 '&' (c5 '&' (c4 '&' c3))))) '&' c8 by BVFUNC_1:7
.= (c2 '&' c8) '&' (c7 '&' (c6 '&' (c5 '&' (c4 '&' c3)))) by BVFUNC_1:7
.= ((c2 '&' c8) '&' c7) '&' (c6 '&' (c5 '&' (c4 '&' c3))) by BVFUNC_1:7
.= (((c2 '&' c8) '&' c7) '&' c6) '&' (c5 '&' (c4 '&' c3)) by BVFUNC_1:7
.= ((((c2 '&' c8) '&' c7) '&' c6) '&' c5) '&' (c4 '&' c3) by BVFUNC_1:7
.= (((((c2 '&' c8) '&' c7) '&' c6) '&' c5) '&' c4) '&' c3 by BVFUNC_1:7 ;
((((((c2 '&' c8) '&' c7) '&' c6) '&' c5) '&' c4) '&' c3) 'imp' c3 = I_el c1 by BVFUNC_6:39;
hence (((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 '<' c3 by E7, BVFUNC_1:19;
end;

E7: for b1 being non empty set
for b2, b3, b4, b5, b6, b7, b8 being Element of Funcs b1,BOOLEAN holds
( ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b2 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b3 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b4 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b5 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b6 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b7 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b8 = I_el b1 )
proof
let c1 be non empty set ;
let c2, c3, c4, c5, c6, c7, c8 be Element of Funcs c1,BOOLEAN ;
E8: (((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 '<' c2 by E6;
E9: (((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 '<' c3 by E6;
E10: (((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 '<' c4 by E5;
E11: (((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 '<' c5 by E4;
E12: (((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 '<' c6 by E3;
E13: (((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 '<' c7 by E2;
(((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8 '<' c8 by E1;
hence ( ((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c2 = I_el c1 & ((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c3 = I_el c1 & ((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c4 = I_el c1 & ((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c5 = I_el c1 & ((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c6 = I_el c1 & ((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c7 = I_el c1 & ((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c8 = I_el c1 ) by E8, E9, E10, E11, E12, E13, BVFUNC_1:19;
end;

theorem E8: :: BVFUNC_9:1
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds (b2 'or' b3) '&' (b3 'imp' b4) '<' b2 'or' b4
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be Element of c1; :: according to BVFUNC_1:def 15
assume E9: ((c2 'or' c3) '&' (c3 'imp' c4)) . c5 = TRUE ;
E10: ((c2 'or' c3) '&' (c3 'imp' c4)) . c5 = ((c2 'or' c3) . c5) '&' ((c3 'imp' c4) . c5) by VALUAT_1:def 6
.= ((c2 'or' c3) . c5) '&' ((('not' c3) 'or' c4) . c5) by BVFUNC_4:8
.= ((c2 'or' c3) . c5) '&' ((('not' c3) . c5) 'or' (c4 . c5)) by BVFUNC_1:def 7
.= ((c2 . c5) 'or' (c3 . c5)) '&' ((('not' c3) . c5) 'or' (c4 . c5)) by BVFUNC_1:def 7 ;
now
assume (c2 'or' c4) . c5 <> TRUE ;
then (c2 'or' c4) . c5 = FALSE by MARGREL1:43;
then E11: (c2 . c5) 'or' (c4 . c5) = FALSE by BVFUNC_1:def 7;
E12: ( c2 . c5 = TRUE or c2 . c5 = FALSE ) by MARGREL1:39;
( c4 . c5 = TRUE or c4 . c5 = FALSE ) by MARGREL1:39;
then ( c2 . c5 = FALSE & c4 . c5 = FALSE ) by E11, E12, BINARITH:19;
then ((c2 . c5) 'or' (c3 . c5)) '&' ((('not' c3) . c5) 'or' (c4 . c5)) = (c3 . c5) '&' ((('not' c3) . c5) 'or' FALSE ) by BINARITH:7
.= (c3 . c5) '&' (('not' c3) . c5) by BINARITH:7
.= (c3 . c5) '&' ('not' (c3 . c5)) by VALUAT_1:def 5
.= FALSE by MARGREL1:46 ;
hence not verum by E9, E10, MARGREL1:43;
end;
hence (c2 'or' c4) . c5 = TRUE ;
end;

theorem E9: :: BVFUNC_9:2
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 '&' (b2 'imp' b3) '<' b3
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
let c4 be Element of c1; :: according to BVFUNC_1:def 15
assume E10: (c2 '&' (c2 'imp' c3)) . c4 = TRUE ;
E11: (c2 '&' (c2 'imp' c3)) . c4 = (c2 . c4) '&' ((c2 'imp' c3) . c4) by VALUAT_1:def 6
.= (c2 . c4) '&' ((('not' c2) 'or' c3) . c4) by BVFUNC_4:8
.= (c2 . c4) '&' ((('not' c2) . c4) 'or' (c3 . c4)) by BVFUNC_1:def 7
.= ((c2 . c4) '&' (('not' c2) . c4)) 'or' ((c2 . c4) '&' (c3 . c4)) by BINARITH:22
.= ((c2 . c4) '&' ('not' (c2 . c4))) 'or' ((c2 . c4) '&' (c3 . c4)) by VALUAT_1:def 5
.= FALSE 'or' ((c2 . c4) '&' (c3 . c4)) by MARGREL1:46
.= (c2 . c4) '&' (c3 . c4) by BINARITH:7 ;
now
assume c3 . c4 <> TRUE ;
then (c2 . c4) '&' (c3 . c4) = FALSE '&' (c2 . c4) by MARGREL1:43
.= FALSE by MARGREL1:49 ;
hence not verum by E10, E11, MARGREL1:43;
end;
hence c3 . c4 = TRUE ;
end;

theorem :: BVFUNC_9:3
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 'imp' b3) '&' ('not' b3) '<' 'not' b2
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
let c4 be Element of c1; :: according to BVFUNC_1:def 15
assume E10: ((c2 'imp' c3) '&' ('not' c3)) . c4 = TRUE ;
E11: ((c2 'imp' c3) '&' ('not' c3)) . c4 = ((c2 'imp' c3) . c4) '&' (('not' c3) . c4) by VALUAT_1:def 6
.= ((('not' c2) 'or' c3) . c4) '&' (('not' c3) . c4) by BVFUNC_4:8
.= (('not' c3) . c4) '&' ((('not' c2) . c4) 'or' (c3 . c4)) by BVFUNC_1:def 7
.= ((('not' c3) . c4) '&' (('not' c2) . c4)) 'or' ((('not' c3) . c4) '&' (c3 . c4)) by BINARITH:22
.= ((('not' c3) . c4) '&' (('not' c2) . c4)) 'or' (('not' (c3 . c4)) '&' (c3 . c4)) by VALUAT_1:def 5
.= ((('not' c3) . c4) '&' (('not' c2) . c4)) 'or' FALSE by MARGREL1:46
.= (('not' c3) . c4) '&' (('not' c2) . c4) by BINARITH:7 ;
now
assume ('not' c2) . c4 <> TRUE ;
then (('not' c3) . c4) '&' (('not' c2) . c4) = FALSE '&' (('not' c3) . c4) by MARGREL1:43
.= FALSE by MARGREL1:49 ;
hence not verum by E10, E11, MARGREL1:43;
end;
hence ('not' c2) . c4 = TRUE ;
end;

theorem :: BVFUNC_9:4
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 'or' b3) '&' ('not' b2) '<' b3
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
let c4 be Element of c1; :: according to BVFUNC_1:def 15
assume E10: ((c2 'or' c3) '&' ('not' c2)) . c4 = TRUE ;
E11: ((c2 'or' c3) '&' ('not' c2)) . c4 = ((c2 'or' c3) . c4) '&' (('not' c2) . c4) by VALUAT_1:def 6
.= (('not' c2) . c4) '&' ((c2 . c4) 'or' (c3 . c4)) by BVFUNC_1:def 7
.= ((('not' c2) . c4) '&' (c2 . c4)) 'or' ((('not' c2) . c4) '&' (c3 . c4)) by BINARITH:22
.= (('not' (c2 . c4)) '&' (c2 . c4)) 'or' ((('not' c2) . c4) '&' (c3 . c4)) by VALUAT_1:def 5
.= FALSE 'or' ((('not' c2) . c4) '&' (c3 . c4)) by MARGREL1:46
.= (('not' c2) . c4) '&' (c3 . c4) by BINARITH:7 ;
now
assume c3 . c4 <> TRUE ;
then (('not' c2) . c4) '&' (c3 . c4) = FALSE '&' (('not' c2) . c4) by MARGREL1:43
.= FALSE by MARGREL1:49 ;
hence not verum by E10, E11, MARGREL1:43;
end;
hence c3 . c4 = TRUE ;
end;

theorem :: BVFUNC_9:5
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 'imp' b3) '&' (('not' b2) 'imp' b3) '<' b3
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
let c4 be Element of c1; :: according to BVFUNC_1:def 15
assume E10: ((c2 'imp' c3) '&' (('not' c2) 'imp' c3)) . c4 = TRUE ;
E11: ((c2 'imp' c3) '&' (('not' c2) 'imp' c3)) . c4 = ((c2 'imp' c3) . c4) '&' ((('not' c2) 'imp' c3) . c4) by VALUAT_1:def 6
.= ((('not' c2) 'or' c3) . c4) '&' ((('not' c2) 'imp' c3) . c4) by BVFUNC_4:8
.= ((('not' c2) 'or' c3) . c4) '&' ((('not' ('not' c2)) 'or' c3) . c4) by BVFUNC_4:8
.= ((('not' c2) 'or' c3) . c4) '&' ((c2 'or' c3) . c4) by BVFUNC_1:4
.= ((('not' c2) . c4) 'or' (c3 . c4)) '&' ((c2 'or' c3) . c4) by BVFUNC_1:def 7
.= ((('not' c2) . c4) 'or' (c3 . c4)) '&' ((c2 . c4) 'or' (c3 . c4)) by BVFUNC_1:def 7 ;
now
assume c3 . c4 <> TRUE ;
then c3 . c4 = FALSE by MARGREL1:43;
then ((('not' c2) . c4) 'or' (c3 . c4)) '&' ((c2 . c4) 'or' (c3 . c4)) = (('not' c2) . c4) '&' ((c2 . c4) 'or' FALSE ) by BINARITH:7
.= (('not' c2) . c4) '&' (c2 . c4) by BINARITH:7
.= ('not' (c2 . c4)) '&' (c2 . c4) by VALUAT_1:def 5
.= FALSE by MARGREL1:46 ;
hence not verum by E10, E11, MARGREL1:43;
end;
hence c3 . c4 = TRUE ;
end;

theorem :: BVFUNC_9:6
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 'imp' b3) '&' (b2 'imp' ('not' b3)) '<' 'not' b2
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
let c4 be Element of c1; :: according to BVFUNC_1:def 15
assume E10: ((c2 'imp' c3) '&' (c2 'imp' ('not' c3))) . c4 = TRUE ;
E11: ((c2 'imp' c3) '&' (c2 'imp' ('not' c3))) . c4 = ((c2 'imp' c3) . c4) '&' ((c2 'imp' ('not' c3)) . c4) by VALUAT_1:def 6
.= ((('not' c2) 'or' c3) . c4) '&' ((c2 'imp' ('not' c3)) . c4) by BVFUNC_4:8
.= ((('not' c2) 'or' c3) . c4) '&' ((('not' c2) 'or' ('not' c3)) . c4) by BVFUNC_4:8
.= ((('not' c2) . c4) 'or' (c3 . c4)) '&' ((('not' c2) 'or' ('not' c3)) . c4) by BVFUNC_1:def 7
.= ((('not' c2) . c4) 'or' (c3 . c4)) '&' ((('not' c2) . c4) 'or' (('not' c3) . c4)) by BVFUNC_1:def 7 ;
now
assume ('not' c2) . c4 <> TRUE ;
then ('not' c2) . c4 = FALSE by MARGREL1:43;
then ((('not' c2) . c4) 'or' (c3 . c4)) '&' ((('not' c2) . c4) 'or' (('not' c3) . c4)) = (c3 . c4) '&' (FALSE 'or' (('not' c3) . c4)) by BINARITH:7
.= (c3 . c4) '&' (('not' c3) . c4) by BINARITH:7
.= (c3 . c4) '&' ('not' (c3 . c4)) by VALUAT_1:def 5
.= FALSE by MARGREL1:46 ;
hence not verum by E10, E11, MARGREL1:43;
end;
hence ('not' c2) . c4 = TRUE ;
end;

theorem :: BVFUNC_9:7
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'imp' (b3 '&' b4) '<' b2 'imp' b3
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be Element of c1; :: according to BVFUNC_1:def 15
assume E10: (c2 'imp' (c3 '&' c4)) . c5 = TRUE ;
E11: (c2 'imp' (c3 '&' c4)) . c5 = (('not' c2) 'or' (c3 '&' c4)) . c5 by BVFUNC_4:8
.= (('not' c2) . c5) 'or' ((c3 '&' c4) . c5) by BVFUNC_1:def 7
.= (('not' c2) . c5) 'or' ((c3 . c5) '&' (c4 . c5)) by VALUAT_1:def 6 ;
now
assume (c2 'imp' c3) . c5 <> TRUE ;
then (c2 'imp' c3) . c5 = FALSE by MARGREL1:43;
then (('not' c2) 'or' c3) . c5 = FALSE by BVFUNC_4:8;
then E12: (('not' c2) . c5) 'or' (c3 . c5) = FALSE by BVFUNC_1:def 7;
(('not' c2) . c5) 'or' ((c3 . c5) '&' (c4 . c5)) = ((('not' c2) . c5) 'or' (c3 . c5)) '&' ((('not' c2) . c5) 'or' (c4 . c5)) by BINARITH:23
.= FALSE by E12, MARGREL1:49 ;
hence not verum by E10, E11, MARGREL1:43;
end;
hence (c2 'imp' c3) . c5 = TRUE ;
end;

theorem :: BVFUNC_9:8
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds (b2 'or' b3) 'imp' b4 '<' b2 'imp' b4
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be Element of c1; :: according to BVFUNC_1:def 15
assume E10: ((c2 'or' c3) 'imp' c4) . c5 =