:: 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))))
.= ((c2 . c4) 'or' ('not' (c3 . c4))) '&' (('not' (c2 . c4)) 'or' (c3 . c4))
.= (((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 c2 = c3 by BVFUNC_1:20;
hence ( c2 'imp' c3 = I_el c1 & c3 'imp' c2 = I_el c1 ) by BVFUNC_1:19;
end;
assume ( c2 'imp' c3 = I_el c1 & c3 'imp' c2 = I_el c1 ) ;
then c2 'eqv' c3 = (I_el c1) '&' (I_el c1) by E2;
hence c2 'eqv' c3 = I_el c1 by BVFUNC_1:9;
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 ) ) by BVFUNC_1:20;

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 'eqv' c3 = I_el c1 ;
then c2 = c3 by BVFUNC_1:20;
hence ('not' c2) 'eqv' ('not' c3) = I_el c1 by BVFUNC_1:20;
end;

theorem :: BVFUNC_4:13
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN holds
( ( b2 'eqv' b3 = I_el b1 & b4 'eqv' b5 = I_el b1 ) implies ( (b2 '&' b4) 'eqv' (b3 '&' b5) = I_el b1 ) )
proof
let c1 be non empty set ;
let c2, c3, c4, c5 be Element of Funcs c1,BOOLEAN ;
assume ( c2 'eqv' c3 = I_el c1 & c4 'eqv' c5 = I_el c1 ) ;
then ( c2 = c3 & c4 = c5 ) by BVFUNC_1:20;
hence (c2 '&' c4) 'eqv' (c3 '&' c5) = I_el c1 by BVFUNC_1:20;
end;

theorem :: BVFUNC_4:14
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN holds
( ( b2 'eqv' b3 = I_el b1 & b4 'eqv' b5 = I_el b1 ) implies ( (b2 'imp' b4) 'eqv' (b3 'imp' b5) = I_el b1 ) )
proof
let c1 be non empty set ;
let c2, c3, c4, c5 be Element of Funcs c1,BOOLEAN ;
assume ( c2 'eqv' c3 = I_el c1 & c4 'eqv' c5 = I_el c1 ) ;
then ( c2 = c3 & c4 = c5 ) by BVFUNC_1:20;
hence (c2 'imp' c4) 'eqv' (c3 'imp' c5) = I_el c1 by BVFUNC_1:20;
end;

theorem :: BVFUNC_4:15
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN holds
( ( b2 'eqv' b3 = I_el b1 & b4 'eqv' b5 = I_el b1 ) implies ( (b2 'or' b4) 'eqv' (b3 'or' b5) = I_el b1 ) )
proof
let c1 be non empty set ;
let c2, c3, c4, c5 be Element of Funcs c1,BOOLEAN ;
assume ( c2 'eqv' c3 = I_el c1 & c4 'eqv' c5 = I_el c1 ) ;
then ( c2 = c3 & c4 = c5 ) by BVFUNC_1:20;
hence (c2 'or' c4) 'eqv' (c3 'or' c5) = I_el c1 by BVFUNC_1:20;
end;

theorem :: BVFUNC_4:16
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN holds
( ( b2 'eqv' b3 = I_el b1 & b4 'eqv' b5 = I_el b1 ) implies ( (b2 'eqv' b4) 'eqv' (b3 'eqv' b5) = I_el b1 ) )
proof
let c1 be non empty set ;
let c2, c3, c4, c5 be Element of Funcs c1,BOOLEAN ;
assume ( c2 'eqv' c3 = I_el c1 & c4 'eqv' c5 = I_el c1 ) ;
then ( c2 = c3 & c4 = c5 ) by BVFUNC_1:20;
hence (c2 'eqv' c4) 'eqv' (c3 'eqv' c5) = I_el c1 by BVFUNC_1:20;
end;

theorem :: BVFUNC_4:17
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN
for b4 being Subset of (PARTITIONS b1)
for b5 being a_partition of b1 holds All (b2 'eqv' b3),b5,b4 = (All (b2 'imp' b3),b5,b4) '&' (All (b3 'imp' b2),b5,b4)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
let c4 be Subset of (PARTITIONS c1);
let c5 be a_partition of c1;
E5: for b1 being Element of c1 holds (All (c2 'eqv' c3),c5,c4) . b1 = ((All (c2 'imp' c3),c5,c4) '&' (All (c3 'imp' c2),c5,c4)) . b1
proof
let c6 be Element of c1;
(All (c2 'eqv' c3),c5,c4) . c6 = (All ((c2 'imp' c3) '&' (c3 'imp' c2)),c5,c4) . c6 by E2
.= ((All (c2 'imp' c3),c5,c4) '&' (All (c3 'imp' c2),c5,c4)) . c6 by BVFUNC_2:13 ;
hence (All (c2 'eqv' c3),c5,c4) . c6 = ((All (c2 'imp' c3),c5,c4) '&' (All (c3 'imp' c2),c5,c4)) . c6 ;
end;
consider c6 being Function such that
E6: ( All (c2 'eqv' c3),c5,c4 = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
consider c7 being Function such that
E7: ( (All (c2 'imp' c3),c5,c4) '&' (All (c3 'imp' c2),c5,c4) = c7 & dom c7 = c1 & rng c7 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c6 & c1 = dom c7 & ( for b1 being set holds
( b1 in c1 implies c6 . b1 = c7 . b1 ) ) ) by E5, E6, E7;
hence All (c2 'eqv' c3),c5,c4 = (All (c2 'imp' c3),c5,c4) '&' (All (c3 'imp' c2),c5,c4) by E6, E7, FUNCT_1:9;
end;

theorem :: BVFUNC_4:18
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 holds All b2,b4,b3 '<' Ex b2,b5,b3
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
let c3 be Subset of (PARTITIONS c1);
let c4, c5 be a_partition of c1;
thus All c2,c4,c3 '<' Ex c2,c5,c3
proof
E5: All c2,c4,c3 '<' c2 by BVFUNC_2:11;
c2 '<' Ex c2,c5,c3 by BVFUNC_2:12;
hence All c2,c4,c3 '<' Ex c2,c5,c3 by E5, BVFUNC_1:18;
end;
end;

theorem :: BVFUNC_4:19
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN
for b4 being Subset of (PARTITIONS b1)
for b5 being a_partition of b1 holds
( ( b4 is independent & b5 in b4 & b3 is_independent_of b5,b4 & b2 'imp' b3 = I_el b1 ) implies ( (All b2,b5,b4) 'imp' b3 = I_el b1 ) )
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
let c4 be Subset of (PARTITIONS c1);
let c5 be a_partition of c1;
assume E5: ( c4 is independent & c5 in c4 & c3 is_independent_of c5,c4 & c2 'imp' c3 = I_el c1 ) ;
E6: All c2,c5,c4 = B_INF c2,(CompF c5,c4) by BVFUNC_2:def 9;
for b1 being Element of c1 holds ((All c2,c5,c4) 'imp' c3) . b1 = TRUE
proof
let c6 be Element of c1;
(c2 'imp' c3) . c6 = TRUE by E5, BVFUNC_1:def 14;
then E7: ('not' (c2 . c6)) 'or' (c3 . c6) = TRUE by BVFUNC_1:def 11;
E8: ( 'not' (c2 . c6) = TRUE or 'not' (c2 . c6) = FALSE ) by MARGREL1:39;
now
per cases ( 'not' (c2 . c6) = TRUE or c3 . c6 = TRUE ) by E7, E8, BINARITH:7;
case 'not' (c2 . c6) = TRUE ;
then c2 . c6