let Y be non empty set ; :: thesis: for PA being a_partition of Y
for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) holds
Intersect F is_a_dependent_set_of PA

let PA be a_partition of Y; :: thesis: for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) holds
Intersect F is_a_dependent_set_of PA

let F be Subset-Family of Y; :: thesis: ( Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )

per cases ( F = {} or F <> {} ) ;
suppose F = {} ; :: thesis: ( Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )

then Intersect F = Y by SETFAM_1:def 9;
hence ( Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA ) by Th7; :: thesis: verum
end;
suppose A1: F <> {} ; :: thesis: ( Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )

then reconsider F9 = F as non empty Subset-Family of Y ;
assume that
A2: Intersect F <> {} and
A3: for X being set st X in F holds
X is_a_dependent_set_of PA ; :: thesis:
defpred S1[ object , object ] means ex A being set st
( A = \$2 & A c= PA & \$2 <> {} & \$1 = union A );
A4: for X being object st X in F holds
ex B being object st S1[X,B]
proof
let x be object ; :: thesis: ( x in F implies ex B being object st S1[x,B] )
reconsider X = x as set by TARSKI:1;
assume x in F ; :: thesis: ex B being object st S1[x,B]
then X is_a_dependent_set_of PA by A3;
then ex B being set st
( B c= PA & B <> {} & X = union B ) ;
then ex B being object st S1[X,B] ;
hence ex B being object st S1[x,B] ; :: thesis: verum
end;
consider f being Function such that
A5: ( dom f = F & ( for X being object st X in F holds
S1[X,f . X] ) ) from rng f c= bool (bool Y)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in bool (bool Y) )
reconsider yy = y as set by TARSKI:1;
assume y in rng f ; :: thesis: y in bool (bool Y)
then consider x being object such that
A6: x in dom f and
A7: y = f . x by FUNCT_1:def 3;
S1[x,f . x] by A5, A6;
then f . x c= PA ;
then yy c= bool Y by ;
hence y in bool (bool Y) ; :: thesis: verum
end;
then reconsider f = f as Function of F9,(bool (bool Y)) by ;
defpred S2[ set ] means \$1 in F;
deffunc H1( Element of F9) -> Element of bool (bool Y) = f . \$1;
reconsider T = { H1(X) where X is Element of F9 : S2[X] } as Subset-Family of (bool Y) from reconsider T = T as Subset-Family of (bool Y) ;
take B = Intersect T; :: according to PARTIT1:def 1 :: thesis: ( B c= PA & B <> {} & Intersect F = union B )
thus B c= PA :: thesis: ( B <> {} & Intersect F = union B )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in PA )
assume A8: x in B ; :: thesis: x in PA
consider X being object such that
A9: X in F by ;
f . X in T by A9;
then A10: x in f . X by ;
S1[X,f . X] by A5, A9;
then f . X c= PA ;
hence x in PA by A10; :: thesis: verum
end;
thus B <> {} :: thesis:
proof
consider X being object such that
A11: X in F by ;
A12: f . X in T by A11;
consider A being object such that
A13: A in Intersect F by ;
reconsider A = A as Element of Y by A13;
set AA = EqClass (A,PA);
A14: A in meet F by ;
for X being set st X in T holds
EqClass (A,PA) in X
proof
let X be set ; :: thesis: ( X in T implies EqClass (A,PA) in X )
assume X in T ; :: thesis: EqClass (A,PA) in X
then consider z being Element of F9 such that
A15: X = f . z and
z in F ;
A16: S1[z,f . z] by A5;
then A17: f . z c= PA ;
( z = union (f . z) & A in z ) by ;
then ex A0 being set st
( A in A0 & A0 in f . z ) by TARSKI:def 4;
hence EqClass (A,PA) in X by ; :: thesis: verum
end;
then EqClass (A,PA) in meet T by ;
hence B <> {} by SETFAM_1:def 9; :: thesis: verum
end;
A18: Intersect F c= union B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersect F or x in union B )
assume A19: x in Intersect F ; :: thesis: x in union B
then A20: x in meet F by ;
reconsider x = x as Element of Y by A19;
reconsider PA = PA as a_partition of Y ;
set A = EqClass (x,PA);
consider X being object such that
A21: X in F by ;
A22: f . X in T by A21;
for X being set st X in T holds
EqClass (x,PA) in X
proof
let X be set ; :: thesis: ( X in T implies EqClass (x,PA) in X )
assume X in T ; :: thesis: EqClass (x,PA) in X
then consider z being Element of F9 such that
A23: X = f . z and
z in F ;
A24: S1[z,f . z] by A5;
then A25: f . z c= PA ;
z = union (f . z) by A24;
then x in union (f . z) by ;
then ex A0 being set st
( x in A0 & A0 in f . z ) by TARSKI:def 4;
hence EqClass (x,PA) in X by ; :: thesis: verum
end;
then EqClass (x,PA) in meet T by ;
then ( x in EqClass (x,PA) & EqClass (x,PA) in Intersect T ) by ;
hence x in union B by TARSKI:def 4; :: thesis: verum
end;
union B c= Intersect F
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union B or x in Intersect F )
assume A26: x in union B ; :: thesis:
consider X being object such that
A27: X in F by ;
A28: f . X in T by A27;
consider y being set such that
A29: x in y and
A30: y in B by ;
A31: y in meet T by ;
for X being set st X in F holds
x in X
proof
let X be set ; :: thesis: ( X in F implies x in X )
assume A32: X in F ; :: thesis: x in X
then f . X in T ;
then A33: y in f . X by ;
S1[X,f . X] by ;
then X = union (f . X) ;
hence x in X by ; :: thesis: verum
end;
then x in meet F by ;
hence x in Intersect F by ; :: thesis: verum
end;
hence Intersect F = union B by ; :: thesis: verum
end;
end;