:: BVFUNC_4 semantic presentation

theorem :: BVFUNC_4:1
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( b2 '<' b3 'imp' b4 implies b2 '&' b3 '<' b4 )
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
assume E1: c2 '<' c3 'imp' c4 ;
for b1 being Element of c1 holds ((c2 '&' c3) 'imp' c4) . b1 = TRUE
proof
let c5 be Element of c1;
E2: c2 'imp' (c3 'imp' c4) = I_el c1 by E1, BVFUNC_1:19;
E3: (c2 'imp' (c3 'imp' c4)) . c5 = ('not' (c2 . c5)) 'or' ((c3 'imp' c4) . c5) by BVFUNC_1:def 11
.= ('not' (c2 . c5)) 'or' (('not' (c3 . c5)) 'or' (c4 . c5)) by BVFUNC_1:def 11
.= (('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5) by BINARITH:20 ;
((c2 '&' c3) 'imp' c4) . c5 = ('not' ((c2 '&' c3) . c5)) 'or' (c4 . c5) by BVFUNC_1:def 11
.= ('not' ((c2 . c5) '&' (c3 . c5))) 'or' (c4 . c5) by VALUAT_1:def 6
.= (('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5) by BINARITH:9 ;
hence ((c2 '&' c3) 'imp' c4) . c5 = TRUE by E2, E3, BVFUNC_1:def 14;
end;
then (c2 '&' c3) 'imp' c4 = I_el c1 by BVFUNC_1:def 14;
hence c2 '&' c3 '<' c4 by BVFUNC_1:19;
end;

theorem :: BVFUNC_4:2
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( b2 '&' b3 '<' b4 implies b2 '<' b3 'imp' b4 )
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
assume E1: c2 '&' c3 '<' c4 ;
for b1 being Element of c1 holds (c2 'imp' (c3 'imp' c4)) . b1 = TRUE
proof
let c5 be Element of c1;
E2: (c2 '&' c3) 'imp' c4 = I_el c1 by E1, BVFUNC_1:19;
E3: (c2 'imp' (c3 'imp' c4)) . c5 = ('not' (c2 . c5)) 'or' ((c3 'imp' c4) . c5) by BVFUNC_1:def 11
.= ('not' (c2 . c5)) 'or' (('not' (c3 . c5)) 'or' (c4 . c5)) by BVFUNC_1:def 11
.= (('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5) by BINARITH:20 ;
((c2 '&' c3) 'imp' c4) . c5 = ('not' ((c2 '&' c3) . c5)) 'or' (c4 . c5) by BVFUNC_1:def 11
.= ('not' ((c2 . c5) '&' (c3 . c5))) 'or' (c4 . c5) by VALUAT_1:def 6
.= (('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5) by BINARITH:9 ;
hence (c2 'imp' (c3 'imp' c4)) . c5 = TRUE by E2, E3, BVFUNC_1:def 14;
end;
then c2 'imp' (c3 'imp' c4) = I_el c1 by BVFUNC_1:def 14;
hence c2 '<' c3 'imp' c4 by BVFUNC_1:19;
end;

theorem :: BVFUNC_4:3
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'or' (b2 '&' b3) = b2
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds (c2 'or' (c2 '&' c3)) . b1 = c2 . b1
proof
let c4 be Element of c1;
E2: (c2 'or' (c2 '&' c3)) . c4 = (c2 . c4) 'or' ((c2 '&' c3) . c4) by BVFUNC_1:def 7
.= (c2 . c4) 'or' ((c2 . c4) '&' (c3 . c4)) by VALUAT_1:def 6 ;
now
per cases ( c2 . c4 = TRUE or c2 . c4 = FALSE ) by MARGREL1:39;
case c2 . c4 = TRUE ;
hence (c2 'or' (c2 '&' c3)) . c4 = c2 . c4 by E2, BINARITH:19;
end;
case E3: c2 . c4 = FALSE ;
then (c2 'or' (c2 '&' c3)) . c4 = FALSE 'or' FALSE by E2, MARGREL1:45
.= FALSE by BINARITH:7 ;
hence (c2 'or' (c2 '&' c3)) . c4 = c2 . c4 by E3;
end;
end;
end;
hence (c2 'or' (c2 '&' c3)) . c4 = c2 . c4 ;
end;
consider c4 being Function such that
E2: ( c2 'or' (c2 '&' c3) = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
consider c5 being Function such that
E3: ( c2 = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in c1 implies c4 . b1 = c5 . b1 ) by E1, E2, E3;
hence c2 'or' (c2 '&' c3) = c2 by E2, E3, FUNCT_1:9;
end;

theorem :: BVFUNC_4:4
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 '&' (b2 'or' b3) = b2
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds (c2 '&' (c2 'or' c3)) . b1 = c2 . b1
proof
let c4 be Element of c1;
E2: (c2 '&' (c2 'or' c3)) . c4 = (c2 . c4) '&' ((c2 'or' c3) . c4) by VALUAT_1:def 6
.= (c2 . c4) '&' ((c2 . c4) 'or' (c3 . c4)) by BVFUNC_1:def 7 ;
now
per cases ( c2 . c4 = TRUE or c2 . c4 = FALSE ) by MARGREL1:39;
case E3: c2 . c4 = TRUE ;
then (c2 '&' (c2 'or' c3)) . c4 = TRUE '&' TRUE by E2, BINARITH:19
.= TRUE by MARGREL1:45 ;
hence (c2 '&' (c2 'or' c3)) . c4 = c2 . c4 by E3;
end;
case c2 . c4 = FALSE ;
hence (c2 '&' (c2 'or' c3)) . c4 = c2 . c4 by E2, MARGREL1:45;
end;
end;
end;
hence (c2 '&' (c2 'or' c3)) . c4 = c2 . c4 ;
end;
consider c4 being Function such that
E2: ( c2 '&' (c2 'or' c3) = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
consider c5 being Function such that
E3: ( c2 = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in c1 implies c4 . b1 = c5 . b1 ) by E1, E2, E3;
hence c2 '&' (c2 'or' c3) = c2 by E2, E3, FUNCT_1:9;
end;

theorem E1: :: BVFUNC_4:5
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds b2 '&' ('not' b2) = O_el b1
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
E2: for b1 being Element of c1 holds (c2 '&' ('not' c2)) . b1 = (O_el c1) . b1
proof
let c3 be Element of c1;
E3: (c2 '&' ('not' c2)) . c3 = (c2 . c3) '&' (('not' c2) . c3) by VALUAT_1:def 6
.= (c2 . c3) '&' ('not' (c2 . c3)) by VALUAT_1:def 5 ;
E4: ( 'not' FALSE = TRUE & 'not' TRUE = FALSE ) by MARGREL1:41;
E5: (O_el c1) . c3 = FALSE by BVFUNC_1:def 13;
now
per cases ( c2 . c3 = TRUE or c2 . c3 = FALSE ) by MARGREL1:39;
case c2 . c3 = TRUE ;
hence (c2 '&' ('not' c2)) . c3 = (O_el c1) . c3 by E3, E4, E5, MARGREL1:45;
end;
case c2 . c3 = FALSE ;
hence (c2 '&' ('not' c2)) . c3 = (O_el c1) . c3 by E3, E5, MARGREL1:45;
end;
end;
end;
hence (c2 '&' ('not' c2)) . c3 = (O_el c1) . c3 ;
end;
consider c3 being Function such that
E3: ( c2 '&' ('not' c2) = c3 & dom c3 = c1 & rng c3 c= BOOLEAN ) by FUNCT_2:def 2;
consider c4 being Function such that
E4: ( O_el c1 = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in c1 implies c3 . b1 = c4 . b1 ) by E2, E3, E4;
hence c2 '&' ('not' c2) = O_el c1 by E3, E4, FUNCT_1:9;
end;

theorem :: BVFUNC_4:6
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds b2 'or' ('not' b2) = I_el b1
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
E2: for b1 being Element of c1 holds (c2 'or' ('not' c2)) . b1 = (I_el c1) . b1
proof
let c3 be Element of c1;
(c2 'or' ('not' c2)) . c3 = (c2 . c3) 'or' (('not' c2) . c3) by BVFUNC_1:def 7
.= (c2 . c3) 'or' ('not' (c2 . c3)) by VALUAT_1:def 5
.= TRUE by BINARITH:18 ;
hence (c2 'or' ('not' c2)) . c3 = (I_el c1) . c3 by BVFUNC_1:def 14;
end;
consider c3 being Function such that
E3: ( c2 'or' ('not' c2) = c3 & dom c3 = c1 & rng c3 c= BOOLEAN ) by FUNCT_2:def 2;
consider c4 being Function such that
E4: ( I_el c1 = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in c1 implies c3 . b1 = c4 . b1 ) by E2, E3, E4;
hence c2 'or' ('not' c2) = I_el c1 by E3, E4, FUNCT_1:9;
end;

theorem E2: :: BVFUNC_4:7
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'eqv' b3 = (b2 'imp' b3) '&' (b3 'imp' b2)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E3: for b1 being Element of c1 holds (c2 'eqv' c3) . b1 = ((c2 'imp' c3) '&' (c3 'imp' c2)) . b1
proof
let c4 be Element of c1;
(c2 'eqv' c3) . c4 = 'not' ((c2 . c4) 'xor' (c3 . c4)) by BVFUNC_1:def 12
.= 'not' ((('not' (c2 . c4)) '&' (c3 . c4)) 'or' ((c2 . c4) '&' ('not' (c3 . c4)))) by BINARITH:def 2
.= ('not' (('not' (c2 . c4)) '&' (c3 . c4))) '&' ('not' ((c2 . c4) '&' ('not' (c3 . c4)))) by BINARITH:10
.= (('not' ('not' (c2 . c4))) 'or' ('not' (c3 . c4))) '&' ('not' ((c2 . c4) '&' ('not' (c3 . c4)))) by BINARITH:9
.= (('not' ('not' (c2 . c4))) 'or' ('not' (c3 . c4))) '&' (('not' (c2 . c4)) 'or' ('not' ('not' (c3 . c4)))) by BINARITH:9
.= ((c2 . c4) 'or' ('not' (c3 . c4))) '&' (('not' (c2 . c4)) 'or' ('not' ('not' (c3 . c4)))) by MARGREL1:40
.= ((c2 . c4) 'or' ('not' (c3 . c4))) '&' (('not' (c2 . c4)) 'or' (c3 . c4)) by MARGREL1:40
.= (((c2 . c4) 'or' ('not' (c3 . c4))) '&' ('not' (c2 . c4))) 'or' (((c2 . c4) 'or' ('not' (c3 . c4))) '&' (c3 . c4)) by BINARITH:22
.= ((('not' (c2 . c4)) '&' (c2 . c4)) 'or' (('not' (c2 . c4)) '&' ('not' (c3 . c4)))) 'or' ((c3 . c4) '&' ((c2 . c4) 'or' ('not' (c3 . c4)))) by BINARITH:22
.= ((('not' (c2 . c4)) '&' (c2 . c4)) 'or' (('not' (c2 . c4)) '&' ('not' (c3 . c4)))) 'or' (((c3 . c4) '&' (c2 . c4)) 'or' ((c3 . c4) '&' ('not' (c3 . c4)))) by BINARITH:22
.= (FALSE 'or' (('not' (c2 . c4)) '&' ('not' (c3 . c4)))) 'or' (((c3 . c4) '&' (c2 . c4)) 'or' ((c3 . c4) '&' ('not' (c3 . c4)))) by MARGREL1:46
.= (FALSE 'or' (('not' (c2 . c4)) '&' ('not' (c3 . c4)))) 'or' (((c3 . c4) '&' (c2 . c4)) 'or' FALSE ) by MARGREL1:46
.= (('not' (c2 . c4)) '&' ('not' (c3 . c4))) 'or' (((c3 . c4) '&' (c2 . c4)) 'or' FALSE ) by BINARITH:7
.= (('not' (c2 . c4)) '&' ('not' (c3 . c4))) 'or' ((c3 . c4) '&' (c2 . c4)) by BINARITH:7
.= ((('not' (c2 . c4)) '&' ('not' (c3 . c4))) 'or' (c3 . c4)) '&' ((('not' (c2 . c4)) '&' ('not' (c3 . c4))) 'or' (c2 . c4)) by BINARITH:23
.= (((c3 . c4) 'or' ('not' (c2 . c4))) '&' ((c3 . c4) 'or' ('not' (c3 . c4)))) '&' ((c2 . c4) 'or' (('not' (c2 . c4)) '&' ('not' (c3 . c4)))) by BINARITH:23
.= (((c3 . c4) 'or' ('not' (c2 . c4))) '&' ((c3 . c4) 'or' ('not' (c3 . c4)))) '&' (((c2 . c4) 'or' ('not' (c2 . c4))) '&' ((c2 . c4) 'or' ('not' (c3 . c4)))) by BINARITH:23
.= (((c3 . c4) 'or' ('not' (c2 . c4))) '&' TRUE ) '&' (((c2 . c4) 'or' ('not' (c2 . c4))) '&' ((c2 . c4) 'or' ('not' (c3 . c4)))) by BINARITH:18
.= (((c3 . c4) 'or' ('not' (c2 . c4))) '&' TRUE ) '&' (TRUE '&' ((c2 . c4) 'or' ('not' (c3 . c4)))) by BINARITH:18
.= ((c3 . c4) 'or' ('not' (c2 . c4))) '&' (TRUE '&' ((c2 . c4) 'or' ('not' (c3 . c4)))) by MARGREL1:50
.= ((c3 . c4) 'or' ('not' (c2 . c4))) '&' ((c2 . c4) 'or' ('not' (c3 . c4))) by MARGREL1:50
.= ((c2 'imp' c3) . c4) '&' (('not' (c3 . c4)) 'or' (c2 . c4)) by BVFUNC_1:def 11
.= ((c2 'imp' c3) . c4) '&' ((c3 'imp' c2) . c4) by BVFUNC_1:def 11
.= ((c2 'imp' c3) '&' (c3 'imp' c2)) . c4 by VALUAT_1:def 6 ;
hence (c2 'eqv' c3) . c4 = ((c2 'imp' c3) '&' (c3 'imp' c2)) . c4 ;
end;
consider c4 being Function such that
E4: ( c2 'eqv' c3 = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
consider c5 being Function such that
E5: ( (c2 'imp' c3) '&' (c3 'imp' c2) = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in c1 implies c4 . b1 = c5 . b1 ) by E3, E4, E5;
hence c2 'eqv' c3 = (c2 'imp' c3) '&' (c3 'imp' c2) by E4, E5, FUNCT_1:9;
end;

theorem E3: :: BVFUNC_4:8
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'imp' b3 = ('not' b2) 'or' b3
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E4: for b1 being Element of c1 holds (c2 'imp' c3) . b1 = (('not' c2) 'or' c3) . b1
proof
let c4 be Element of c1;
(c2 'imp' c3) . c4 = ('not' (c2 . c4)) 'or' (c3 . c4) by BVFUNC_1:def 11
.= (('not' c2) . c4) 'or' (c3 . c4) by VALUAT_1:def 5
.= (('not' c2) 'or' c3) . c4 by BVFUNC_1:def 7 ;
hence (c2 'imp' c3) . c4 = (('not' c2) 'or' c3) . c4 ;
end;
consider c4 being Function such that
E5: ( c2 'imp' c3 = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
consider c5 being Function such that
E6: ( ('not' c2) 'or' c3 = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in c1 implies c4 . b1 = c5 . b1 ) by E4, E5, E6;
hence c2 'imp' c3 = ('not' c2) 'or' c3 by E5, E6, FUNCT_1:9;
end;

theorem :: BVFUNC_4:9
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'xor' b3 = (('not' b2) '&' b3) 'or' (b2 '&' ('not' b3))
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E4: for b1 being Element of c1 holds (c2 'xor' c3) . b1 = ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) . b1
proof
let c4 be Element of c1;
(c2 'xor' c3) . c4 = (c2 . c4) 'xor' (c3 . c4) by BVFUNC_1:def 8
.= (('not' (c2 . c4)) '&' (c3 . c4)) 'or' ((c2 . c4) '&' ('not' (c3 . c4))) by BINARITH:def 2
.= ((('not' c2) . c4) '&' (c3 . c4)) 'or' ((c2 . c4) '&' ('not' (c3 . c4))) by VALUAT_1:def 5
.= ((('not' c2) . c4) '&' (c3 . c4)) 'or' ((c2 . c4) '&' (('not' c3) . c4)) by VALUAT_1:def 5
.= ((('not' c2) '&' c3) . c4) 'or' ((c2 . c4) '&' (('not' c3) . c4)) by VALUAT_1:def 6
.= ((('not' c2) '&' c3) . c4) 'or' ((c2 '&' ('not' c3)) . c4) by VALUAT_1:def 6
.= ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) . c4 by BVFUNC_1:def 7 ;
hence (c2 'xor' c3) . c4 = ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) . c4 ;
end;
consider c4 being Function such that
E5: ( c2 'xor' c3 = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
consider c5 being Function such that
E6: ( (('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)) = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in c1 implies c4 . b1 = c5 . b1 ) by E4, E5, E6;
hence c2 'xor' c3 = (('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)) by E5, E6, FUNCT_1:9;
end;

theorem E4: :: BVFUNC_4:10
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds
( b2 'eqv' b3 = I_el b1 iff ( b2 'imp' b3 = I_el b1 & b3 'imp' b2 = I_el b1 ) )
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
thus ( c2 'eqv' c3 = I_el c1 implies ( c2 'imp' c3 = I_el c1 & c3 'imp' c2 = I_el c1 ) )
proof
assume c2 'eqv' c3 = I_el c1 ;
then E5: (c2 'imp' c3) '&' (c3 'imp' c2) = I_el c1 by E2;
E6: for b1 being Element of c1 holds (c2 'imp' c3) . b1 = TRUE
proof
let c4 be Element of c1;
((c2 'imp' c3) '&' (c3 'imp' c2)) . c4 = TRUE by E5, BVFUNC_1:def 14;
then ((c2 'imp' c3) . c4) '&' ((c3 'imp' c2) . c4) = TRUE by VALUAT_1:def 6;
hence (c2 'imp' c3) . c4 = TRUE by MARGREL1:45;
end;
for b1 being Element of c1 holds (c3 'imp' c2) . b1 = TRUE
proof
let c4 be Element of c1;
((c2 'imp' c3) '&' (c3 'imp' c2)) . c4 = TRUE by E5, BVFUNC_1:def 14;
then ((c2 'imp' c3) . c4) '&' ((c3 'imp' c2) . c4) = TRUE by VALUAT_1:def 6;
hence (c3 'imp' c2) . c4 = TRUE by MARGREL1:45;
end;
hence ( c2 'imp' c3 = I_el c1 & c3 'imp' c2 = I_el c1 ) by E6, BVFUNC_1:def 14;
end;
assume E5: ( c2 'imp' c3 = I_el c1 & c3 'imp' c2 = I_el c1 ) ;
E6: for b1 being Element of c1 holds ((c2 'imp' c3) '&' (c3 'imp' c2)) . b1 = TRUE
proof
let c4 be Element of c1;
E7: (c3 'imp' c2) . c4 = TRUE by E5, BVFUNC_1:def 14;
((c2 'imp' c3) '&' (c3 'imp' c2)) . c4 = ((c2 'imp' c3) . c4) '&' ((c3 'imp' c2) . c4) by VALUAT_1:def 6
.= TRUE by E5, E7, MARGREL1:45 ;
hence ((c2 'imp' c3) '&' (c3 'imp' c2)) . c4 = TRUE ;
end;
c2 'eqv' c3 = (c2 'imp' c3) '&' (c3 'imp' c2) by E2;
hence c2 'eqv' c3 = I_el c1 by E6, BVFUNC_1:def 14;
end;

theorem :: BVFUNC_4:11
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( ( b2 'eqv' b3 = I_el b1 & b3 'eqv' b4 = I_el b1 ) implies ( b2 'eqv' b4 = I_el b1 ) )
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
assume E5: ( c2 'eqv' c3 = I_el c1 & c3 'eqv' c4 = I_el c1 ) ;
then E6: ( c2 'imp' c3 = I_el c1 & c3 'imp' c2 = I_el c1 ) by E4;
E7: ( c3 'imp' c4 = I_el c1 & c4 'imp' c3 = I_el c1 ) by E5, E4;
for b1 being Element of c1 holds (c2 'imp' c4) . b1 = TRUE
proof
let c5 be Element of c1;
(c2 'imp' c3) . c5 = TRUE by E6, BVFUNC_1:def 14;
then E8: ('not' (c2 . c5)) 'or' (c3 . c5) = TRUE by BVFUNC_1:def 11;
E9: ( 'not' (c2 . c5) = TRUE or 'not' (c2 . c5) = FALSE ) by MARGREL1:39;
(c3 'imp' c4) . c5 = TRUE by E7, BVFUNC_1:def 14;
then E10: ('not' (c3 . c5)) 'or' (c4 . c5) = TRUE by BVFUNC_1:def 11;
E11: ( 'not' (c3 . c5) = TRUE or 'not' (c3 . c5) = FALSE ) by MARGREL1:39;
E12: (c2 'imp' c4) . c5 = ('not' (c2 . c5)) 'or' (c4 . c5) by BVFUNC_1:def 11;
now
per cases not ( not ( 'not' (c2 . c5) = TRUE & 'not' (c3 . c5) = TRUE ) & not ( 'not' (c2 . c5) = TRUE & c4 . c5 = TRUE ) & not ( c3 . c5 = TRUE & 'not' (c3 . c5) = TRUE ) & not ( c3 . c5 = TRUE & c4 . c5 = TRUE ) ) by E8, E9, E10, E11, BINARITH:7;
case ( 'not' (c2 . c5) = TRUE & 'not' (c3 . c5) = TRUE ) ;
hence (c2 'imp' c4) . c5 = TRUE by E12, BINARITH:19;
end;
case ( 'not' (c2 . c5) = TRUE & c4 . c5 = TRUE ) ;
hence (c2 'imp' c4) . c5 = TRUE by E12, BINARITH:19;
end;
case E13: ( c3 . c5 = TRUE & 'not' (c3 . c5) = TRUE ) ;
then c3 . c5 = FALSE by MARGREL1:41;
hence (c2 'imp' c4) . c5 = TRUE by E13, MARGREL1:43;
end;
case ( c3 . c5 = TRUE & c4 . c5 = TRUE ) ;
hence (c2 'imp' c4) . c5 = TRUE by E12, BINARITH:19;
end;
end;
end;
hence (c2 'imp' c4) . c5 = TRUE ;
end;
then E8: c2 'imp' c4 = I_el c1 by BVFUNC_1:def 14;
for b1 being Element of c1 holds (c4 'imp' c2) . b1 = TRUE
proof
let c5 be Element of c1;
(c4 'imp' c3) . c5 = TRUE by E7, BVFUNC_1:def 14;
then E9: ('not' (c4 . c5)) 'or' (c3 . c5) = TRUE by BVFUNC_1:def 11;
E10: ( 'not' (c4 . c5) = TRUE or 'not' (c4 . c5) = FALSE ) by MARGREL1:39;
(c3 'imp' c2) . c5 = TRUE by E6, BVFUNC_1:def 14;
then E11: ('not' (c3 . c5)) 'or' (c2 . c5) = TRUE by BVFUNC_1:def 11;
E12: ( 'not' (c3 . c5) = TRUE or 'not' (c3 . c5) = FALSE ) by MARGREL1:39;
E13: (c4 'imp' c2) . c5 = ('not' (c4 . c5)) 'or' (c2 . c5) by BVFUNC_1:def 11;
now
per cases not ( not ( 'not' (c4 . c5) = TRUE & 'not' (c3 . c5) = TRUE ) & not ( 'not' (c4 . c5) = TRUE & c2 . c5 = TRUE ) & not ( c3 . c5 = TRUE & 'not' (c3 . c5) = TRUE ) & not ( c3 . c5 = TRUE & c2 . c5 = TRUE ) ) by E9, E10, E11, E12, BINARITH:7;
case ( 'not' (c4 . c5) = TRUE & 'not' (c3 . c5) = TRUE ) ;
hence (c4 'imp' c2) . c5 = TRUE by E13, BINARITH:19;
end;
case ( 'not' (c4 . c5) = TRUE & c2 . c5 = TRUE ) ;
hence (c4 'imp' c2) . c5 = TRUE by E13, BINARITH:19;
end;
case E14: ( c3 . c5 = TRUE & 'not' (c3 . c5) = TRUE ) ;
then c3 . c5 = FALSE by MARGREL1:41;
hence (c4 'imp' c2) . c5 = TRUE by E14, MARGREL1:43;
end;
case ( c3 . c5 = TRUE & c2 . c5 = TRUE ) ;
hence (c4 'imp' c2) . c5 = TRUE by E13, BINARITH:19;
end;
end;
end;
hence (c4 'imp' c2) . c5 = TRUE ;
end;
then c4 'imp' c2 = I_el c1 by BVFUNC_1:def 14;
hence c2 'eqv' c4 = I_el c1 by E8, E4;
end;

theorem :: BVFUNC_4:12
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds
( b2 'eqv' b3 = I_el b1 implies ('not' b2) 'eqv' ('not' b3) = I_el b1 )
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
assume c2 'eq