:: BVFUNC11 semantic presentation

theorem E1: :: BVFUNC11:1
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being a_partition of b1 holds
( b3 '<' b4 implies EqClass b2,b3 c= EqClass b2,b4 )
proof
let c1 be non empty set ;
let c2 be Element of c1;
let c3, c4 be a_partition of c1;
assume E2: c3 '<' c4 ;
E3: ( c2 in EqClass c2,c3 & EqClass c2,c3 in c3 ) by T_1TOPSP:def 1;
ex b1 being set st
( b1 in c4 & EqClass c2,c3 c= b1 ) by E2, SETFAM_1:def 2;
hence EqClass c2,c3 c= EqClass c2,c4 by E3, T_1TOPSP:def 1;
end;

theorem :: BVFUNC11:2
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being a_partition of b1 holds EqClass b2,b3 c= EqClass b2,(b3 '\/' b4)
proof
let c1 be non empty set ;
let c2 be Element of c1;
let c3, c4 be a_partition of c1;
c3 '<' c3 '\/' c4 by PARTIT1:19;
hence EqClass c2,c3 c= EqClass c2,(c3 '\/' c4) by E1;
end;

theorem :: BVFUNC11:3
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being a_partition of b1 holds EqClass b2,(b3 '/\' b4) c= EqClass b2,b3
proof
let c1 be non empty set ;
let c2 be Element of c1;
let c3, c4 be a_partition of c1;
c3 '>' c3 '/\' c4 by PARTIT1:17;
hence EqClass c2,(c3 '/\' c4) c= EqClass c2,c3 by E1;
end;

theorem :: BVFUNC11:4
for b1 being non empty set
for b2 being Element of b1
for b3 being a_partition of b1 holds
( EqClass b2,b3 c= EqClass b2,(%O b1) & EqClass b2,(%I b1) c= EqClass b2,b3 )
proof
let c1 be non empty set ;
let c2 be Element of c1;
let c3 be a_partition of c1;
( %O c1 '>' c3 & c3 '>' %I c1 ) by PARTIT1:36;
hence ( EqClass c2,c3 c= EqClass c2,(%O c1) & EqClass c2,(%I c1) c= EqClass c2,c3 ) by E1;
end;

theorem :: BVFUNC11:5
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being a_partition of b1 holds
( ( b2 is independent & b2 = {b3,b4} ) implies ( not b3 <> b4 or for b5, b6 being set holds
not ( b5 in b3 & b6 in b4 & not b5 meets b6 ) ) )
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4 be a_partition of c1;
assume that E2: c2 is independent
and E3: ( c2 = {c3,c4} & c3 <> c4 ) ;
let c5, c6 be set ;
assume E4: ( c5 in c3 & c6 in c4 ) ;
set c7 = c3,c4 --> c5,c6;
{c5,c6} c= bool c1
proof
let c8 be set ; :: uses TARSKI:def 3
assume c8 in {c5,c6} ;
then ( c8 = c5 or c8 = c6 ) by TARSKI:def 2;
hence c8 in bool c1 by E4;
end;
then reconsider c8 = {c5,c6} as Subset-Family of c1 ;
E5: ( dom (c3,c4 --> c5,c6) = {c3,c4} & rng (c3,c4 --> c5,c6) = c8 ) by E3, FUNCT_4:65, FUNCT_4:67;
for b1 being set holds
( b1 in c2 implies (c3,c4 --> c5,c6) . b1 in b1 )
proof
let c9 be set ;
assume c9 in c2 ;
then ( c9 = c3 or c9 = c4 ) by E3, TARSKI:def 2;
hence (c3,c4 --> c5,c6) . c9 in c9 by E3, E4, FUNCT_4:66;
end;
then Intersect c8 <> {} by E2, E3, E5, BVFUNC_2:def 5;
hence c5 /\ c6 <> {} by E4, MSSUBFAM:10; :: uses XBOOLE_0:def 7
end;

theorem :: BVFUNC11:6
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being a_partition of b1 holds
( ( b2 is independent & b2 = {b3,b4} ) implies ( not b3 <> b4 or '/\' b2 = b3 '/\' b4 ) )
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4 be a_partition of c1;
assume that E2: c2 is independent
and E3: ( c2 = {c3,c4} & c3 <> c4 ) ;
E4: c3 '/\' c4 c= '/\' c2
proof
let c5 be set ; :: uses TARSKI:def 3
assume c5 in c3 '/\' c4 ;
then c5 in (INTERSECTION c3,c4) \ {{} } by PARTIT1:def 4;
then ( c5 in INTERSECTION c3,c4 & not c5 in {{} } ) by XBOOLE_0:def 4;
then consider c6, c7 being set such that
E5: ( c6 in c3 & c7 in c4 & c5 = c6 /\ c7 ) by SETFAM_1:def 5;
set c8 = c3,c4 --> c6,c7;
{c6,c7} c= bool c1
proof
let c9 be set ; :: uses TARSKI:def 3
assume c9 in {c6,c7} ;
then ( c9 = c6 or c9 = c7 ) by TARSKI:def 2;
hence c9 in bool c1 by E5;
end;
then reconsider c9 = {c6,c7} as Subset-Family of c1 ;
E6: ( dom (c3,c4 --> c6,c7) = {c3,c4} & rng (c3,c4 --> c6,c7) = c9 ) by E3, FUNCT_4:65, FUNCT_4:67;
E7: for b1 being set holds
( b1 in c2 implies (c3,c4 --> c6,c7) . b1 in b1 )
proof
let c10 be set ;
assume c10 in c2 ;
then ( c10 = c3 or c10 = c4 ) by E3, TARSKI:def 2;
hence (c3,c4 --> c6,c7) . c10 in c10 by E3, E5, FUNCT_4:66;
end;
then E8: Intersect c9 <> {} by E2, E3, E6, BVFUNC_2:def 5;
c6 /\ c7 = Intersect c9 by E5, MSSUBFAM:10;
hence c5 in '/\' c2 by E3, E5, E6, E7, E8, BVFUNC_2:def 1;
end;
'/\' c2 c= c3 '/\' c4
proof
let c5 be set ; :: uses TARSKI:def 3
assume c5 in '/\' c2 ;
then consider c6 being Function, c7 being Subset-Family of c1 such that
E5: ( dom c6 = c2 & rng c6 = c7 & for b1 being set holds
( b1 in c2 implies c6 . b1 in b1 ) & c5 = Intersect c7 & c5 <> {} ) by BVFUNC_2:def 1;
E6: ( c3 in c2 & c4 in c2 ) by E3, TARSKI:def 2;
then E7: ( c6 . c3 in c3 & c6 . c4 in c4 ) by E5;
E8: ( c6 . c3 in rng c6 & c6 . c4 in rng c6 ) by E5, E6, FUNCT_1:def 5;
then E9: Intersect c7 = meet (rng c6) by E5, SETFAM_1:def 10;
E10: not c5 in {{} } by E5, TARSKI:def 1;
E11: (c6 . c3) /\ (c6 . c4) c= c5
proof
let c8 be set ; :: uses TARSKI:def 3
assume c8 in (c6 . c3) /\ (c6 . c4) ;
then E12: ( c8 in c6 . c3 & c8 in c6 . c4 ) by XBOOLE_0:def 3;
rng c6 = {(c6 . c3),(c6 . c4)}
proof
thus rng c6 c= {(c6 . c3),(c6 . c4)} :: uses XBOOLE_0:def 10
proof
let c9 be set ; :: uses TARSKI:def 3
assume c9 in rng c6 ;
then consider c10 being set such that
E13: ( c10 in dom c6 & c9 = c6 . c10 ) by FUNCT_1:def 5;
( c10 = c3 or c10 = c4 ) by E3, E5, E13, TARSKI:def 2;
hence c9 in {(c6 . c3),(c6 . c4)} by E13, TARSKI:def 2;
end;
let c9 be set ; :: uses TARSKI:def 3
assume c9 in {(c6 . c3),(c6 . c4)} ;
then E13: ( c9 = c6 . c3 or c9 = c6 . c4 ) by TARSKI:def 2;
( c3 in dom c6 & c4 in dom c6 ) by E3, E5, TARSKI:def 2;
hence c9 in rng c6 by E13, FUNCT_1:def 5;
end;
then for b1 being set holds
( b1 in rng c6 implies c8 in b1 ) by E12, TARSKI:def 2;
hence c8 in c5 by E5, E8, E9, SETFAM_1:def 1;
end;
c5 c= (c6 . c3) /\ (c6 . c4)
proof
let c8 be set ; :: uses TARSKI:def 3
assume c8 in c5 ;
then ( c8 in c6 . c3 & c8 in c6 . c4 ) by E5, E8, E9, SETFAM_1:def 1;
hence c8 in (c6 . c3) /\ (c6 . c4) by XBOOLE_0:def 3;
end;
then (c6 . c3) /\ (c6 . c4) = c5 by E11, XBOOLE_0:def 10;
then c5 in INTERSECTION c3,c4 by E7, SETFAM_1:def 5;
then c5 in (INTERSECTION c3,c4) \ {{} } by E10, XBOOLE_0:def 4;
hence c5 in c3 '/\' c4 by PARTIT1:def 4;
end;
hence '/\' c2 = c3 '/\' c4 by E4, XBOOLE_0:def 10;
end;

theorem :: BVFUNC11:7
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being a_partition of b1 holds
( ( b2 = {b3,b4} ) implies ( not b3 <> b4 or CompF b3,b2 = b4 ) )
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4 be a_partition of c1;
assume E2: ( c2 = {c3,c4} & c3 <> c4 ) ;
then E3: c2 \ {c3} = ({c3} \/ {c4}) \ {c3} by ENUMSET1:41
.= ({c3} \ {c3}) \/ ({c4} \ {c3}) by XBOOLE_1:42
.= ({c3} \ {c3}) \/ {c4} by E2, ZFMISC_1:20 ;
c3 in {c3} by TARSKI:def 1;
then {c3} \ {c3} = {} by ZFMISC_1:68;
then E4: CompF c3,c2 = '/\' {c4} by E3, BVFUNC_2:def 7;
E5: '/\' {c4} c= c4
proof
let c5 be set ; :: uses TARSKI:def 3
assume c5 in '/\' {c4} ;
then consider c6 being Function, c7 being Subset-Family of c1 such that
E6: ( dom c6 = {c4} & rng c6 = c7 & for b1 being set holds
( b1 in {c4} implies c6 . b1 in b1 ) & c5 = Intersect c7 & c5 <> {} ) by BVFUNC_2:def 1;
rng c6 = {(c6 . c4)} by E6, FUNCT_1:14;
then E7: c5 = meet {(c6 . c4)} by E6, SETFAM_1:def 10;
c4 in {c4} by TARSKI:def 1;
then c6 . c4 in c4 by E6;
hence c5 in c4 by E7, SETFAM_1:11;
end;
c4 c= '/\' {c4}
proof
let c5 be set ; :: uses TARSKI:def 3
assume E6: c5 in c4 ;
set c6 = c4 .--> c5;
E7: ( dom (c4 .--> c5) = {c4} & rng (c4 .--> c5) = {c5} ) by CQC_LANG:5;
E8: for b1 being set holds
( b1 in {c4} implies (c4 .--> c5) . b1 in b1 )
proof
let c7 be set ;
assume c7 in {c4} ;
then c7 = c4 by TARSKI:def 1;
hence (c4 .--> c5) . c7 in c7 by E6, CQC_LANG:6;
end;
rng (c4 .--> c5) c= bool c1
proof
let c7 be set ; :: uses TARSKI:def 3
assume c7 in rng (c4 .--> c5) ;
then c7 = c5 by E7, TARSKI:def 1;
hence c7 in bool c1 by E6;
end;
then reconsider c7 = rng (c4 .--> c5) as Subset-Family of c1 ;
meet c7 = Intersect c7 by E7, SETFAM_1:def 10;
then E9: c5 = Intersect c7 by E7, SETFAM_1:11;
c5 <> {} by E6, EQREL_1:def 6;
hence c5 in '/\' {c4} by E7, E8, E9, BVFUNC_2:def 1;
end;
hence CompF c3,c2 = c4 by E4, E5, XBOOLE_0:def 10;
end;

theorem E2: :: BVFUNC11:8
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
( b2 '<' b3 implies All b2,b5,b4 '<' Ex b3,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;
assume c2 '<' c3 ;
then E3: All c2,c5,c4 '<' All c3,c5,c4 by PARTIT_2:13;
All c3,c5,c4 '<' Ex c3,c5,c4 by BVFUNC_4:18;
hence All c2,c5,c4 '<' Ex c3,c5,c4 by E3, BVFUNC_1:18;
end;

theorem :: BVFUNC11:9
canceled;

theorem :: BVFUNC11:10
canceled;

theorem :: BVFUNC11:11
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
( b3 is independent implies All (All b2,b4,b3),b5,b3 '<' Ex (All b2,b5,b3),b4,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;
assume c3 is independent ;
then All (All c2,c4,c3),c5,c3 = All (All c2,c5,c3),c4,c3 by PARTIT_2:17;
hence All (All c2,c4,c3),c5,c3 '<' Ex (All c2,c5,c3),c4,c3 by E2;
end;

theorem :: BVFUNC11:12
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 (All b2,b4,b3),b5,b3 '<' Ex (Ex b2,b5,b3),b4,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;
E3: All (All c2,c4,c3),c5,c3 '<' All c2,c4,c3 by BVFUNC_2:11;
c2 '<' Ex c2,c5,c3 by BVFUNC_2:12;
then All c2,c4,c3 '<' Ex (Ex c2,c5,c3),c4,c3 by E2;
hence All (All c2,c4,c3),c5,c3 '<' Ex (Ex c2,c5,c3),c4,c3 by E3, BVFUNC_1:18;
end;

theorem :: BVFUNC11:13
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
( b3 is independent implies All (All b2,b4,b3),b5,b3 '<' All (Ex b2,b5,b3),b4,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;
assume c3 is independent ;
then E3: All (All c2,c4,c3),c5,c3 = All (All c2,c5,c3),c4,c3 by PARTIT_2:17;
All c2,c5,c3 '<' Ex c2,c5,c3 by E2;
hence All (All c2,c4,c3),c5,c3 '<' All (Ex c2,c5,c3),c4,c3 by E3, PARTIT_2:13;
end;

theorem :: BVFUNC11:14
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 (Ex b2,b4,b3),b5,b3 '<' Ex (Ex b2,b5,b3),b4,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;
E3: Ex c2,c5,c3 = B_SUP c2,(CompF c5,c3) by BVFUNC_2:def 10;
let c6 be Element of c1; :: uses BVFUNC_1:def 15
assume E4: (All (Ex c2,c4,c3),c5,c3) . c6 = TRUE ;
E5: ( c6 in EqClass c6,(CompF c5,c3) & EqClass c6,(CompF c5,c3) in CompF c5,c3 ) by T_1TOPSP:def 1;
E6: now
assume ex b1 being Element of c1 st
( b1 in EqClass c6,(CompF c5,c3) & not (Ex c2,c4,c3) . b1 = TRUE ) ;
then (B_INF (Ex c2,c4,c3),(CompF c5,c3)) . c6 = FALSE by BVFUNC_1:def 19;
then (All (Ex c2,c4,c3),c5,c3) . c6 = FALSE by BVFUNC_2:def 9;
hence not verum by E4, MARGREL1:43;
end;
now
assume for b1 being Element of c1 holds
not ( b1 in EqClass c6,(CompF c4,c3) & c2 . b1 = TRUE ) ;
then (B_SUP c2,(CompF c4,c3)) . c6 = FALSE by BVFUNC_1:def 20;
then (Ex c2,c4,c3) . c6 = FALSE by BVFUNC_2:def 10;
then (Ex c2,c4,c3) . c6 <> TRUE by MARGREL1:43;
hence not verum by E5, E6;
end;
then consider c7 being Element of c1 such that
E7: ( c7 in EqClass c6,(CompF c4,c3) & c2 . c7 = TRUE ) ;
c7 in EqClass c7,(CompF c5,c3) by T_1TOPSP:def 1;
then (Ex c2,c5,c3) . c7 = TRUE by E3, E7, BVFUNC_1:def 20;
then (B_SUP (Ex c2,c5,c3),(CompF c4,c3)) . c6 = TRUE by E7, BVFUNC_1:def 20;
hence (Ex (Ex c2,c5,c3),c4,c3) . c6 = TRUE by BVFUNC_2:def 10;
end;

theorem :: BVFUNC11:15
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 'not' (Ex (All b2,b4,b3),b5,b3) '<' Ex (Ex ('not' b2),b5,b3),b4,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;
E3: All c2,c4,c3 = B_INF c2,(CompF c4,c3) by BVFUNC_2:def 9;
E4: Ex ('not' c2),c5,c3 = B_SUP ('not' c2),(CompF c5,c3) by BVFUNC_2:def 10;
E5: Ex (All c2,c4,c3),c5,c3 = B_SUP (All c2,c4,c3),(CompF c5,c3) by BVFUNC_2:def 10;
let c6 be Element of c1; :: uses BVFUNC_1:def 15
assume ('not' (Ex (All c2,c4,c3),c5,c3)) . c6 = TRUE ;
then 'not' ((Ex (All c2,c4,c3),c5,c3) . c6) = TRUE by VALUAT_1:def 5;
then (Ex (All c2,c4,c3),c5,c3) . c6 = FALSE by MARGREL1:41;
then E6: (Ex (All c2,c4,c3),c5,c3) . c6 <> TRUE by MARGREL1:43;
( c6 in EqClass c6,(CompF c5,c3) & EqClass c6,(CompF c5,c3) in CompF c5,c3 ) by T_1TOPSP:def 1;
then (All c2,c4,c3) . c6 <> TRUE by E5, E6, BVFUNC_1:def 20;
then consider c7 being Element of c1 such that
E7: ( c7 in EqClass c6,(CompF c4,c3) & c2 . c7 <> TRUE ) by E3, BVFUNC_1:def 19;
E8: ( c7 in EqClass c7,(CompF c5,c3) & EqClass c7,(CompF c5,c3) in CompF c5,c3 ) by T_1TOPSP:def 1;
c2 . c7 = FALSE by E7, MARGREL1:43;
then ('not' c2) . c7 = 'not' FALSE by VALUAT_1:def 5;
then ('not' c2) . c7 = TRUE by MARGREL1:41;
then (Ex ('not' c2),c5,c3) . c7 = TRUE by E4, E8, BVFUNC_1:def 20;
then (B_SUP (Ex ('not' c2),c5,c3),(CompF c4,c3)) . c6 = TRUE by E7, BVFUNC_1:def 20;
hence (Ex (Ex ('not' c2),c5,c3),c4,c3) . c6 = TRUE by BVFUNC_2:def 10;
end;

theorem E3: :: BVFUNC11:16
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
( b3 is independent implies Ex ('not' (All b2,b4,b3)),b5,b3 '<' Ex (Ex ('not' b2),b5,b3),b4,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;
assume c3 is independent ;
then Ex (Ex ('not' c2),c5,c3),c4,c3 = Ex (Ex ('not' c2),c4,c3),c5,c3 by PARTIT_2:18;
hence Ex ('not' (All c2,c4,c3)),c5,c3 '<' Ex (Ex ('not' c2),c5,c3),c4,c3 by BVFUNC_2:20;
end;

theorem E4: :: BVFUNC11:17
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
( b3 is independent implies 'not' (All (All b2,b4,b3),b5,b3) = Ex ('not' (All b2,b5,b3)),b4,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;
assume c3 is independent ;
then All (All c2,c4,c3),c5,c3 = All (All c2,c5,c3),c4,c3 by PARTIT_2:17;
hence 'not' (All (All c2,c4,c3),c5,c3) = Ex ('not' (All c2,c5,c3)),c4,c3 by BVFUNC_2:20;
end;

theorem :: BVFUNC11: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
( b3 is independent implies All ('not' (All b2,b4,b3)),b5,b3 '<' Ex (Ex ('not' b2),b5,b3),b4,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;
assume c3 is independent ;
then E5: Ex (Ex ('not' c2),c5,c3),c4,c3 = Ex (Ex ('not' c2),c4,c3),c5,c3 by PARTIT_2:18;
'not' (All c2,c4,c3) = Ex ('not' c2),c4,c3 by BVFUNC_2:20;
hence All ('not' (All c2,c4,c3)),c5,c3 '<' Ex (Ex ('not' c2),c5,c3),c4,c3 by E5, E2;
end;

theorem :: BVFUNC11:19
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
( b3 is independent implies 'not' (All (All b2,b4,b3),b5,b3) = Ex (Ex ('not' b2),b5,b3),b4,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;
assume E5: c3 is independent ;
Ex ('not' c2),c5,c3 = 'not' (All c2,c5,c3) by BVFUNC_2:20;
hence 'not' (All (All c2,c4,c3),c5,c3) = Ex (Ex ('not' c2),c5,c3),c4,c3 by E5, E4;
end;

theorem :: BVFUNC11:20
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
( b3 is independent implies 'not' (All (All b2,b4,b3),b5,b3) '<' Ex (Ex ('not' b2),b4,b3),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;
assume E5: c3 is independent ;
then Ex ('not' (All c2,c5,c3)),c4,c3 '<' Ex (Ex ('not' c2),c4,c3),c5,c3 by E3;
hence 'not' (All (All c2,c4,c3),c5,c3) '<' Ex (Ex ('not' c2),c4,c3),c5,c3 by E5, E4;
end;

theorem :: BVFUNC11:21
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 'not' (All (Ex b2,b4,b3),b5,b3) = Ex (All ('not' b2),b4,b3),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;
'not' (All (Ex c2,c4,c3),c5,c3) = Ex ('not' (Ex c2,c4,c3)),c5,c3 by BVFUNC_2:20;
hence 'not' (All (Ex c2,c4,c3),c5,c3) = Ex (All ('not' c2),c4,c3),c5,c3 by BVFUNC_2:21;
end;

theorem :: BVFUNC11:22
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 'not' (Ex (All b2,b4,b3),b5,b3) = All (Ex ('not' b2),b4,b3),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;
'not' (Ex (All c2,c4,c3),c5,c3) = All ('not' (All c2,c4,c3)),c5,c3 by BVFUNC_2:21;
hence 'not' (Ex (All c2,c4,c3),c5,c3) = All (Ex ('not' c2),c4,c3),c5,c3 by BVFUNC_2:20;
end;

theorem :: BVFUNC11:23
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 'not' (All (All b2,b4,b3),b5,b3) = Ex (Ex ('not' b2),b4,b3),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;
Ex ('not' (All c2,c4,c3)),c5,c3 = Ex (Ex ('not' c2),c4,c3),c5,c3 by BVFUNC_2:20;
hence 'not' (All (All c2,c4,c3),c5,c3) = Ex (Ex ('not' c2),c4,c3),c5,c3 by BVFUNC_2:20;
end;

theorem :: BVFUNC11:24
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
( b3 is independent implies Ex (All b2,b4,b3),b5,b3 '<' Ex (Ex b2,b5,b3),b4,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;
assume c3 is independent ;
then E5: Ex (Ex c2,c5,c3),c4,c3 = Ex (Ex c2,c4,c3),c5,c3 by PARTIT_2:18;
All c2,c4,c3 '<' Ex c2,c4,c3 by E2;
hence Ex (All c2,c4,c3),c5,c3 '<' Ex (Ex c2,c5,c3),c4,c3 by E5, PARTIT_2:15;
end;

theorem :: BVFUNC11:25
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 (All b2,b4,b3),b5,b3 '<' All (Ex b2,b4,b3),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;
All c2,c4,c3 '<' Ex c2,c4,c3 by E2;
hence All (All c2,c4,c3),c5,c3 '<' All (Ex c2,c4,c3),c5,c3 by PARTIT_2:13;
end;

theorem :: BVFUNC11:26
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 (All b2,b4,b3),b5,b3 '<' Ex (Ex b2,b4,b3),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;
All c2,c4,c3 '<' Ex c2,c4,c3 by E2;
hence All (All c2,c4,c3),c5,c3 '<' Ex (Ex c2,c4,c3),c5,c3 by E2;
end;

theorem :: BVFUNC11:27
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 Ex (All b2,b4,b3),b5,b3 '<' Ex (Ex b2,b4,b3),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;
All c2,c4,c3 '<' Ex c2,c4,c3 by E2;
hence Ex (All c2,c4,c3),c5,c3 '<' Ex (Ex c2,c4,c3),c5,c3 by PARTIT_2:15;
end;