:: BVFUNC_3 semantic presentation

theorem Th1: :: BVFUNC_3:1
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds b3 'imp' b4 '<' (All b3,b5,b2) 'imp' (Ex b4,b5,b2)
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be a_partition of c1;
let c6 be Element of c1; :: according to BVFUNC_1:def 15
assume (c3 'imp' c4) . c6 = TRUE ;
then E1: ('not' (c3 . c6)) 'or' (c4 . c6) = TRUE by BVFUNC_1:def 11;
E2: ( 'not' (c3 . c6) = TRUE or 'not' (c3 . c6) = FALSE ) by MARGREL1:39;
E3: ( c6 in EqClass c6,(CompF c5,c2) & EqClass c6,(CompF c5,c2) in CompF c5,c2 ) by T_1TOPSP:def 1;
per cases ( 'not' (c3 . c6) = TRUE or c4 . c6 = TRUE ) by E1, E2, BINARITH:7;
suppose 'not' (c3 . c6) = TRUE ;
then c3 . c6 = FALSE by MARGREL1:41;
then c3 . c6 <> TRUE by MARGREL1:43;
then (B_INF c3,(CompF c5,c2)) . c6 = FALSE by E3, BVFUNC_1:def 19;
then (All c3,c5,c2) . c6 = FALSE by BVFUNC_2:def 9;
hence ((All c3,c5,c2) 'imp' (Ex c4,c5,c2)) . c6 = ('not' FALSE ) 'or' ((Ex c4,c5,c2) . c6) by BVFUNC_1:def 11
.= TRUE 'or' ((Ex c4,c5,c2) . c6) by MARGREL1:41
.= TRUE by BINARITH:19 ;

end;
suppose c4 . c6 = TRUE ;
then (B_SUP c4,(CompF c5,c2)) . c6 = TRUE by E3, BVFUNC_1:def 20;
then (Ex c4,c5,c2) . c6 = TRUE by BVFUNC_2:def 10;
hence ((All c3,c5,c2) 'imp' (Ex c4,c5,c2)) . c6 = ('not' ((All c3,c5,c2) . c6)) 'or' TRUE by BVFUNC_1:def 11
.= TRUE by BINARITH:19 ;

end;
end;
end;

theorem Th2: :: BVFUNC_3:2
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds (All b3,b5,b2) '&' (All b4,b5,b2) '<' b3 '&' b4
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be a_partition of c1;
let c6 be Element of c1; :: according to BVFUNC_1:def 15
assume E1: ((All c3,c5,c2) '&' (All c4,c5,c2)) . c6 = TRUE ;
E2: ((All c3,c5,c2) '&' (All c4,c5,c2)) . c6 = ((All c3,c5,c2) . c6) '&' ((All c4,c5,c2) . c6) by VALUAT_1:def 6;
E3: ( c6 in EqClass c6,(CompF c5,c2) & EqClass c6,(CompF c5,c2) in CompF c5,c2 ) by T_1TOPSP:def 1;
E4: now
assume ex b1 being Element of c1 st
( b1 in EqClass c6,(CompF c5,c2) & not c3 . b1 = TRUE ) ;
then (B_INF c3,(CompF c5,c2)) . c6 = FALSE by BVFUNC_1:def 19;
then (All c3,c5,c2) . c6 = FALSE by BVFUNC_2:def 9;
then (All c3,c5,c2) . c6 <> TRUE by MARGREL1:43;
hence not verum by E1, E2, MARGREL1:45;
end;
now
assume ex b1 being Element of c1 st
( b1 in EqClass c6,(CompF c5,c2) & not c4 . b1 = TRUE ) ;
then (B_INF c4,(CompF c5,c2)) . c6 = FALSE by BVFUNC_1:def 19;
then (All c4,c5,c2) . c6 = FALSE by BVFUNC_2:def 9;
then (All c4,c5,c2) . c6 <> TRUE by MARGREL1:43;
hence not verum by E1, E2, MARGREL1:45;
end;
then E5: c4 . c6 = TRUE by E3;
thus (c3 '&' c4) . c6 = (c3 . c6) '&' (c4 . c6) by VALUAT_1:def 6
.= TRUE '&' TRUE by E3, E4, E5
.= TRUE by MARGREL1:45 ;
end;

theorem Th3: :: BVFUNC_3:3
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds b3 '&' b4 '<' (Ex b3,b5,b2) '&' (Ex b4,b5,b2)
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be a_partition of c1;
E1: Ex c3,c5,c2 = B_SUP c3,(CompF c5,c2) by BVFUNC_2:def 10;
let c6 be Element of c1; :: according to BVFUNC_1:def 15
assume E2: (c3 '&' c4) . c6 = TRUE ;
(c3 '&' c4) . c6 = (c3 . c6) '&' (c4 . c6) by VALUAT_1:def 6;
then E3: ( c3 . c6 = TRUE & c4 . c6 = TRUE ) by E2, MARGREL1:45;
E4: ( c6 in EqClass c6,(CompF c5,c2) & EqClass c6,(CompF c5,c2) in CompF c5,c2 ) by T_1TOPSP:def 1;
then (B_SUP c4,(CompF c5,c2)) . c6 = TRUE by E3, BVFUNC_1:def 20;
then E5: (Ex c4,c5,c2) . c6 = TRUE by BVFUNC_2:def 10;
thus ((Ex c3,c5,c2) '&' (Ex c4,c5,c2)) . c6 = ((Ex c3,c5,c2) . c6) '&' ((Ex c4,c5,c2) . c6) by VALUAT_1:def 6
.= TRUE '&' TRUE by E1, E3, E4, E5, BVFUNC_1:def 20
.= TRUE by MARGREL1:45 ;
end;

theorem Th4: :: BVFUNC_3:4
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds 'not' ((All b3,b5,b2) '&' (All b4,b5,b2)) = (Ex ('not' b3),b5,b2) 'or' (Ex ('not' b4),b5,b2)
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be a_partition of c1;
E1: All c3,c5,c2 = B_INF c3,(CompF c5,c2) by BVFUNC_2:def 9;
E2: All c4,c5,c2 = B_INF c4,(CompF c5,c2) by BVFUNC_2:def 9;
E3: 'not' ((All c3,c5,c2) '&' (All c4,c5,c2)) '<' (Ex ('not' c3),c5,c2) 'or' (Ex ('not' c4),c5,c2)
proof
let c6 be Element of c1; :: according to BVFUNC_1:def 15
assume ('not' ((All c3,c5,c2) '&' (All c4,c5,c2))) . c6 = TRUE ;
then E4: 'not' (((All c3,c5,c2) '&' (All c4,c5,c2)) . c6) = TRUE by VALUAT_1:def 5;
((All c3,c5,c2) '&' (All c4,c5,c2)) . c6 = ((All c3,c5,c2) . c6) '&' ((All c4,c5,c2) . c6) by VALUAT_1:def 6;
then E5: ((All c3,c5,c2) . c6) '&' ((All c4,c5,c2) . c6) = FALSE by E4, MARGREL1:41;
per cases ( (All c3,c5,c2) . c6 = FALSE or (All c4,c5,c2) . c6 = FALSE ) by E5, MARGREL1:45;
suppose E6: (All c3,c5,c2) . c6 = FALSE ;
now
assume E7: for b1 being Element of c1 holds
( b1 in EqClass c6,(CompF c5,c2) implies c3 . b1 = TRUE ) ;
(All c3,c5,c2) . c6 <> TRUE by E6, MARGREL1:43;
hence not verum by E1, E7, BVFUNC_1:def 19;
end;
then consider c7 being Element of c1 such that
E7: ( c7 in EqClass c6,(CompF c5,c2) & c3 . c7 <> TRUE ) ;
c3 . c7 = FALSE by E7, MARGREL1:43;
then 'not' (c3 . c7) = TRUE by MARGREL1:41;
then ('not' c3) . c7 = TRUE by VALUAT_1:def 5;
then (B_SUP ('not' c3),(CompF c5,c2)) . c6 = TRUE by E7, BVFUNC_1:def 20;
then (Ex ('not' c3),c5,c2) . c6 = TRUE by BVFUNC_2:def 10;
hence ((Ex ('not' c3),c5,c2) 'or' (Ex ('not' c4),c5,c2)) . c6 = TRUE 'or' ((Ex ('not' c4),c5,c2) . c6) by BVFUNC_1:def 7
.= TRUE by BINARITH:19 ;

end;
suppose E6: (All c4,c5,c2) . c6 = FALSE ;
now
assume E7: for b1 being Element of c1 holds
( b1 in EqClass c6,(CompF c5,c2) implies c4 . b1 = TRUE ) ;
(All c4,c5,c2) . c6 <> TRUE by E6, MARGREL1:43;
hence not verum by E2, E7, BVFUNC_1:def 19;
end;
then consider c7 being Element of c1 such that
E7: ( c7 in EqClass c6,(CompF c5,c2) & c4 . c7 <> TRUE ) ;
c4 . c7 = FALSE by E7, MARGREL1:43;
then 'not' (c4 . c7) = TRUE by MARGREL1:41;
then ('not' c4) . c7 = TRUE by VALUAT_1:def 5;
then (B_SUP ('not' c4),(CompF c5,c2)) . c6 = TRUE by E7, BVFUNC_1:def 20;
then (Ex ('not' c4),c5,c2) . c6 = TRUE by BVFUNC_2:def 10;
hence ((Ex ('not' c3),c5,c2) 'or' (Ex ('not' c4),c5,c2)) . c6 = ((Ex ('not' c3),c5,c2) . c6) 'or' TRUE by BVFUNC_1:def 7
.= TRUE by BINARITH:19 ;

end;
end;
end;
(Ex ('not' c3),c5,c2) 'or' (Ex ('not' c4),c5,c2) '<' 'not' ((All c3,c5,c2) '&' (All c4,c5,c2))
proof
let c6 be Element of c1; :: according to BVFUNC_1:def 15
assume E4: ((Ex ('not' c3),c5,c2) 'or' (Ex ('not' c4),c5,c2)) . c6 = TRUE ;
E5: ((Ex ('not' c3),c5,c2) 'or' (Ex ('not' c4),c5,c2)) . c6 = ((Ex ('not' c3),c5,c2) . c6) 'or' ((Ex ('not' c4),c5,c2) . c6) by BVFUNC_1:def 7;
E6: ( (Ex ('not' c4),c5,c2) . c6 = TRUE or (Ex ('not' c4),c5,c2) . c6 = FALSE ) by MARGREL1:39;
per cases ( (Ex ('not' c3),c5,c2) . c6 = TRUE or (Ex ('not' c4),c5,c2) . c6 = TRUE ) by E4, E5, E6, BINARITH:7;
suppose E7: (Ex ('not' c3),c5,c2) . c6 = TRUE ;
now
assume for b1 being Element of c1 holds
not ( b1 in EqClass c6,(CompF c5,c2) & ('not' c3) . b1 = TRUE ) ;
then (B_SUP ('not' c3),(CompF c5,c2)) . c6 = FALSE by BVFUNC_1:def 20;
then (Ex ('not' c3),c5,c2) . c6 = FALSE by BVFUNC_2:def 10;
hence not verum by E7, MARGREL1:43;
end;
then consider c7 being Element of c1 such that
E8: ( c7 in EqClass c6,(CompF c5,c2) & ('not' c3) . c7 = TRUE ) ;
'not' (c3 . c7) = TRUE by E8, VALUAT_1:def 5;
then c3 . c7 = FALSE by MARGREL1:41;
then E9: c3 . c7 <> TRUE by MARGREL1:43;
thus ('not' ((All c3,c5,c2) '&' (All c4,c5,c2))) . c6 = 'not' (((All c3,c5,c2) '&' (All c4,c5,c2)) . c6) by VALUAT_1:def 5
.= 'not' (((All c3,c5,c2) . c6) '&' ((All c4,c5,c2) . c6)) by VALUAT_1:def 6
.= 'not' (FALSE '&' ((All c4,c5,c2) . c6)) by E1, E8, E9, BVFUNC_1:def 19
.= 'not' FALSE by MARGREL1:45
.= TRUE by MARGREL1:41 ;
end;
suppose E7: (Ex ('not' c4),c5,c2) . c6 = TRUE ;
now
assume for b1 being Element of c1 holds
not ( b1 in EqClass c6,(CompF c5,c2) & ('not' c4) . b1 = TRUE ) ;
then (B_SUP ('not' c4),(CompF c5,c2)) . c6 = FALSE by BVFUNC_1:def 20;
then (Ex ('not' c4),c5,c2) . c6 = FALSE by BVFUNC_2:def 10;
hence not verum by E7, MARGREL1:43;
end;
then consider c7 being Element of c1 such that
E8: ( c7 in EqClass c6,(CompF c5,c2) & ('not' c4) . c7 = TRUE ) ;
'not' (c4 . c7) = TRUE by E8, VALUAT_1:def 5;
then c4 . c7 = FALSE by MARGREL1:41;
then E9: c4 . c7 <> TRUE by MARGREL1:43;
thus ('not' ((All c3,c5,c2) '&' (All c4,c5,c2))) . c6 = 'not' (((All c3,c5,c2) '&' (All c4,c5,c2)) . c6) by VALUAT_1:def 5
.= 'not' (((All c3,c5,c2) . c6) '&' ((All c4,c5,c2) . c6)) by VALUAT_1:def 6
.= 'not' (((All c3,c5,c2) . c6) '&' FALSE ) by E2, E8, E9, BVFUNC_1:def 19
.= 'not' FALSE by MARGREL1:45
.= TRUE by MARGREL1:41 ;
end;
end;
end;
hence 'not' ((All c3,c5,c2) '&' (All c4,c5,c2)) = (Ex ('not' c3),c5,c2) 'or' (Ex ('not' c4),c5,c2) by E3, BVFUNC_1:18;
end;

theorem Th5: :: BVFUNC_3:5
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds 'not' ((Ex b3,b5,b2) '&' (Ex b4,b5,b2)) = (All ('not' b3),b5,b2) 'or' (All ('not' b4),b5,b2)
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be a_partition of c1;
E1: All ('not' c3),c5,c2 = B_INF ('not' c3),(CompF c5,c2) by BVFUNC_2:def 9;
E2: All ('not' c4),c5,c2 = B_INF ('not' c4),(CompF c5,c2) by BVFUNC_2:def 9;
E3: Ex c3,c5,c2 = B_SUP c3,(CompF c5,c2) by BVFUNC_2:def 10;
E4: Ex c4,c5,c2 = B_SUP c4,(CompF c5,c2) by BVFUNC_2:def 10;
E5: 'not' ((Ex c3,c5,c2) '&' (Ex c4,c5,c2)) '<' (All ('not' c3),c5,c2) 'or' (All ('not' c4),c5,c2)
proof
let c6 be Element of c1; :: according to BVFUNC_1:def 15
assume ('not' ((Ex c3,c5,c2) '&' (Ex c4,c5,c2))) . c6 = TRUE ;
then 'not' (((Ex c3,c5,c2) '&' (Ex c4,c5,c2)) . c6) = TRUE by VALUAT_1:def 5;
then ((Ex c3,c5,c2) '&' (Ex c4,c5,c2)) . c6 = FALSE by MARGREL1:41;
then E6: ((Ex c3,c5,c2) . c6) '&' ((Ex c4,c5,c2) . c6) = FALSE by VALUAT_1:def 6;
per cases ( (Ex c3,c5,c2) . c6 = FALSE or (Ex c4,c5,c2) . c6 = FALSE ) by E6, MARGREL1:45;
suppose E7: (Ex c3,c5,c2) . c6 = FALSE ;
E8: now
assume E9: ex b1 being Element of c1 st
( b1 in EqClass c6,(CompF c5,c2) & c3 . b1 = TRUE ) ;
(Ex c3,c5,c2) . c6 <> TRUE by E7, MARGREL1:43;
hence not verum by E3, E9, BVFUNC_1:def 20;
end;
E9: now
let c7 be Element of c1;
assume c7 in EqClass c6,(CompF c5,c2) ;
then c3 . c7 <> TRUE by E8;
then c3 . c7 = FALSE by MARGREL1:43;
then 'not' (c3 . c7) = TRUE by MARGREL1:41;
hence ('not' c3) . c7 = TRUE by VALUAT_1:def 5;
end;
thus ((All ('not' c3),c5,c2) 'or' (All ('not' c4),c5,c2)) . c6 = ((All ('not' c3),c5,c2) . c6) 'or' ((All ('not' c4),c5,c2) . c6) by BVFUNC_1:def 7
.= TRUE 'or' ((All ('not' c4),c5,c2) . c6) by E1, E9, BVFUNC_1:def 19
.= TRUE by BINARITH:19 ;
end;
suppose E7: (Ex c4,c5,c2) . c6 = FALSE ;
E8: now
assume E9: ex b1 being Element of c1 st
( b1 in EqClass c6,(CompF c5,c2) & c4 . b1 = TRUE ) ;
(Ex c4,c5,c2) . c6 <> TRUE by E7, MARGREL1:43;
hence not verum by E4, E9, BVFUNC_1:def 20;
end;
E9: now
let c7 be Element of c1;
assume c7 in EqClass c6,(CompF c5,c2) ;
then c4 . c7 <> TRUE by E8;
then c4 . c7 = FALSE by MARGREL1:43;
then 'not' (c4 . c7) = TRUE by MARGREL1:41;
hence ('not' c4) . c7 = TRUE by VALUAT_1:def 5;
end;
thus ((All ('not' c3),c5,c2) 'or' (All ('not' c4),c5,c2)) . c6 = ((All ('not' c3),c5,c2) . c6) 'or' ((All ('not' c4),c5,c2) . c6) by BVFUNC_1:def 7
.= ((All ('not' c3),c5,c2) . c6) 'or' TRUE by E2, E9, BVFUNC_1:def 19
.= TRUE by BINARITH:19 ;
end;
end;
end;
(All ('not' c3),c5,c2) 'or' (All ('not' c4),c5,c2) '<' 'not' ((Ex c3,c5,c2) '&' (Ex c4,c5,c2))
proof
let c6 be Element of c1; :: according to BVFUNC_1:def 15
assume ((All ('not' c3),c5,c2) 'or' (All ('not' c4),c5,c2)) . c6 = TRUE ;
then E6: ((All ('not' c3),c5,c2) . c6) 'or' ((All ('not' c4),c5,c2) . c6) = TRUE by BVFUNC_1:def 7;
E7: ( (All ('not' c4),c5,c2) . c6 = TRUE or (All ('not' c4),c5,c2) . c6 = FALSE ) by MARGREL1:39;
per cases ( (All ('not' c3),c5,c2) . c6 = TRUE or (All ('not' c4),c5,c2) . c6 = TRUE ) by E6, E7, BINARITH:7;
suppose E8: (All ('not' c3),c5,c2) . c6 = TRUE ;
E9: now
assume ex b1 being Element of c1 st
( b1 in EqClass c6,(CompF c5,c2) & not ('not' c3) . b1 = TRUE ) ;
then (B_INF ('not' c3),(CompF c5,c2)) . c6 = FALSE by BVFUNC_1:def 19;
then (All ('not' c3),c5,c2) . c6 = FALSE by BVFUNC_2:def 9;
hence not verum by E8, MARGREL1:43;
end;
E10: now
let c7 be Element of c1;
assume c7 in EqClass c6,(CompF c5,c2) ;
then ('not' c3) . c7 = TRUE by E9;
then 'not' (c3 . c7) = TRUE by VALUAT_1:def 5;
then c3 . c7 = FALSE by MARGREL1:41;
hence c3 . c7 <> TRUE by MARGREL1:43;
end;
thus ('not' ((Ex c3,c5,c2) '&' (Ex c4,c5,c2))) . c6 = 'not' (((Ex c3,c5,c2) '&' (Ex c4,c5,c2)) . c6) by VALUAT_1:def 5
.= 'not' (((Ex c3,c5,c2) . c6) '&' ((Ex c4,c5,c2) . c6)) by VALUAT_1:def 6
.= 'not' (FALSE '&' ((Ex c4,c5,c2) . c6)) by E3, E10, BVFUNC_1:def 20
.= 'not' FALSE by MARGREL1:45
.= TRUE by MARGREL1:41 ;
end;
suppose E8: (All ('not' c4),c5,c2) . c6 = TRUE ;
E9: now
assume ex b1 being Element of c1 st
( b1 in EqClass c6,(CompF c5,c2) & not ('not' c4) . b1 = TRUE ) ;
then (B_INF ('not' c4),(CompF c5,c2)) . c6 = FALSE by BVFUNC_1:def 19;
then (All ('not' c4),c5,c2) . c6 = FALSE by BVFUNC_2:def 9;
hence not verum by E8, MARGREL1:43;
end;
E10: now
let c7 be Element of c1;
assume c7 in EqClass c6,(CompF c5,c2) ;
then ('not' c4) . c7 = TRUE by E9;
then 'not' (c4 . c7) = TRUE by VALUAT_1:def 5;
then c4 . c7 = FALSE by MARGREL1:41;
hence c4 . c7 <> TRUE by MARGREL1:43;
end;
thus ('not' ((Ex c3,c5,c2) '&' (Ex c4,c5,c2))) . c6 = 'not' (((Ex c3,c5,c2) '&' (Ex c4,c5,c2)) . c6) by VALUAT_1:def 5
.= 'not' (((Ex c3,c5,c2) . c6) '&' ((Ex c4,c5,c2) . c6)) by VALUAT_1:def 6
.= 'not' (((Ex c3,c5,c2) . c6) '&' FALSE ) by E4, E10, BVFUNC_1:def 20
.= 'not' FALSE by MARGREL1:45
.= TRUE by MARGREL1:41 ;
end;
end;
end;
hence 'not' ((Ex c3,c5,c2) '&' (Ex c4,c5,c2)) = (All ('not' c3),c5,c2) 'or' (All ('not' c4),c5,c2) by E5, BVFUNC_1:18;
end;

theorem Th6: :: BVFUNC_3:6
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds (All b3,b5,b2) 'or' (All b4,b5,b2) '<' b3 'or' b4
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be a_partition of c1;
let c6 be Element of c1; :: according to BVFUNC_1:def 15
assume ((All c3,c5,c2) 'or' (All c4,c5,c2)) . c6 = TRUE ;
then E1: ((All c3,c5,c2) . c6) 'or' ((All c4,c5,c2) . c6) = TRUE by BVFUNC_1:def 7;
E2: ( (All c3,c5,c2) . c6 = TRUE or (All c3,c5,c2) . c6 = FALSE ) by MARGREL1:39;
E3: ( c6 in EqClass c6,(CompF c5,c2) & EqClass c6,(CompF c5,c2) in CompF c5,c2 ) by T_1TOPSP:def 1;
per cases ( (All c3,c5,c2) . c6 = TRUE or (All c4,c5,c2) . c6 = TRUE ) by E1, E2, BINARITH:7;
suppose E4: (All c3,c5,c2) . c6 = TRUE ;
E5: now
assume ex b1 being Element of c1 st
( b1 in EqClass c6,(CompF c5,c2) & not c3 . b1 = TRUE ) ;
then (B_INF c3,(CompF c5,c2)) . c6 = FALSE by BVFUNC_1:def 19;
then (All c3,c5,c2) . c6 = FALSE by BVFUNC_2:def 9;
hence not verum by E4, MARGREL1:43;
end;
thus (c3 'or' c4) . c6 = (c3 . c6) 'or' (c4 . c6) by BVFUNC_1:def 7
.= TRUE 'or' (c4 . c6) by E3, E5
.= TRUE by BINARITH:19 ;
end;
suppose E4: (All c4,c5,c2) . c6 = TRUE ;
E5: now
assume ex b1 being Element of c1 st
( b1 in EqClass c6,(CompF c5,c2) & not c4 . b1 = TRUE ) ;
then (B_INF c4,(CompF c5,c2)) . c6 = FALSE by BVFUNC_1:def 19;
then (All c4,c5,c2) . c6 = FALSE by BVFUNC_2:def 9;
hence not verum by E4, MARGREL1:43;
end;
thus (c3 'or' c4) . c6 = (c3 . c6) 'or' (c4 . c6) by BVFUNC_1:def 7
.= (c3 . c6) 'or' TRUE by E3, E5
.= TRUE by BINARITH:19 ;
end;
end;
end;

theorem Th7: :: BVFUNC_3:7
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds b3 'or' b4 '<' (Ex b3,b5,b2) 'or' (Ex b4,b5,b2)
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be a_partition of c1;
E1: Ex c3,c5,c2 = B_SUP c3,(CompF c5,c2) by BVFUNC_2:def 10;
E2: Ex c4,c5,c2 = B_SUP c4,(CompF c5,c2) by BVFUNC_2:def 10;
let c6 be Element of c1; :: according to BVFUNC_1:def 15
assume (c3 'or' c4) . c6 = TRUE ;
then E3: (c3 . c6) 'or' (c4 . c6) = TRUE by BVFUNC_1:def 7;
E4: ( c4 . c6 = TRUE or c4 . c6 = FALSE ) by MARGREL1:39;
E5: ( c6 in EqClass c6,(CompF c5,c2) & EqClass c6,(CompF c5,c2) in CompF c5,c2 ) by T_1TOPSP:def 1;
per cases ( c3 . c6 = TRUE or c4 . c6 = TRUE ) by E3, E4, BINARITH:7;
suppose E6: c3 . c6 = TRUE ;
thus ((Ex c3,c5,c2) 'or' (Ex c4,c5,c2)) . c6 = ((Ex c3,c5,c2) . c6) 'or' ((Ex c4,c5,c2) . c6) by BVFUNC_1:def 7
.= TRUE 'or' ((Ex c4,c5,c2) . c6) by E1, E5, E6, BVFUNC_1:def 20
.= TRUE by BINARITH:19 ;
end;
suppose E6: c4 . c6 = TRUE ;
thus ((Ex c3,c5,c2) 'or' (Ex c4,c5,c2)) . c6 = ((Ex c3,c5,c2) . c6) 'or' ((Ex c4,c5,c2) . c6) by BVFUNC_1:def 7
.= ((Ex c3,c5,c2) . c6) 'or' TRUE by E2, E5, E6, BVFUNC_1:def 20
.= TRUE by BINARITH:19 ;
end;
end;
end;

theorem Th8: :: BVFUNC_3:8
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being Element of Funcs b1,BOOLEAN
for b5 being a_partition of b1 holds b3 'xor' b4 '<' ('not' ((Ex ('not' b3),b5,b2) 'xor' (Ex b4,b5,b2))) 'or' ('not' ((Ex b3,b5,b2</