let Y be non empty set ; :: thesis:
let PA be a_partition of Y; :: thesis:
let F be Subset-Family of Y; :: thesis:

end;

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 S₁[ 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 S₁[X,B]

end;

consider f being Function such that
A5: ( dom f = F & ( for X being object st X in F holds
S₁[X,f . X] ) ) from CLASSES1:sch 1(A4);
rng f c= bool (bool Y)

let y be object ; :: according to TARSKI:def 3 :: thesis:
reconsider yy = y as set by TARSKI:1;
assume y in rng f ; :: thesis:
then consider x being object such that
A6: x in dom f and
A7: y = f . x by FUNCT_1:def 3;
S₁[x,f . x] by A5, A6;
then f . x c= PA ;
then yy c= bool Y by A7, XBOOLE_1:1;
hence y in bool (bool Y) ; :: thesis:

end;

then reconsider f = f as Function of F9,(bool (bool Y)) by A5, FUNCT_2:def 1, RELSET_1:4;
defpred S₂[ set ] means $1 in F;
deffunc H₁( Element of F9) -> Element of bool (bool Y) = f . $1;
reconsider T = { H₁(X) where X is Element of F9 : S₂[X] } as Subset-Family of (bool Y) from DOMAIN_1:sch 8();
reconsider T = T as Subset-Family of (bool Y) ;
take B = Intersect T; :: according to PARTIT1:def 1 :: thesis:
thus B c= PA :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in B ; :: thesis:
consider X being object such that
A9: X in F by A1, XBOOLE_0:def 1;
f . X in T by A9;
then A10: x in f . X by A8, SETFAM_1:43;
S₁[X,f . X] by A5, A9;
then f . X c= PA ;
hence x in PA by A10; :: thesis:

end;

consider X being object such that
A11: X in F by A1, XBOOLE_0:def 1;
A12: f . X in T by A11;
consider A being object such that
A13: A in Intersect F by A2, XBOOLE_0:def 1;
reconsider A = A as Element of Y by A13;
set AA = EqClass (A,PA);
A14: A in meet F by A1, A13, SETFAM_1:def 9;
for X being set st X in T holds
EqClass (A,PA) in X

let X be set ; :: thesis:
assume X in T ; :: thesis:
then consider z being Element of F9 such that
A15: X = f . z and
z in F ;
A16: S₁[z,f . z] by A5;
then A17: f . z c= PA ;
( z = union (f . z) & A in z ) by A14, SETFAM_1:def 1, A16;
then ex A0 being set st
( A in A0 & A0 in f . z ) by TARSKI:def 4;
hence EqClass (A,PA) in X by A15, A17, EQREL_1:def 6; :: thesis:

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A19: x in Intersect F ; :: thesis:
then A20: x in meet F by A1, SETFAM_1:def 9;
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 A1, XBOOLE_0:def 1;
A22: f . X in T by A21;
for X being set st X in T holds
EqClass (x,PA) in X

let X be set ; :: thesis:
assume X in T ; :: thesis:
then consider z being Element of F9 such that
A23: X = f . z and
z in F ;
A24: S₁[z,f . z] by A5;
then A25: f . z c= PA ;
z = union (f . z) by A24;
then x in union (f . z) by A20, SETFAM_1:def 1;
then ex A0 being set st
( x in A0 & A0 in f . z ) by TARSKI:def 4;
hence EqClass (x,PA) in X by A23, A25, EQREL_1:def 6; :: thesis:

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: x in union B ; :: thesis:
consider X being object such that
A27: X in F by A1, XBOOLE_0:def 1;
A28: f . X in T by A27;
consider y being set such that
A29: x in y and
A30: y in B by A26, TARSKI:def 4;
A31: y in meet T by A28, A30, SETFAM_1:def 9;
for X being set st X in F holds
x in X

end;

end;

end;