A1: union PA = Y by EQREL_1:def 6;
A2: for A being set st A in PA holds
( A <> {} & ( for B being set holds
( not B in PA or A = B or A misses B ) ) ) by EQREL_1:def 6;
defpred S₁[ set ] means $1 is_min_depend PA,PB;
consider X being set such that
A3: for d being set holds
( d in X iff ( d in bool Y & S₁[d] ) ) from XBOOLE_0:sch 1();
A4: for d being set holds
( d in X iff d is_min_depend PA,PB )

proof

let d be set ; :: thesis: ( d in X iff d is_min_depend PA,PB )
A5: for d being set st d is_min_depend PA,PB holds
d in bool Y

proof

let d be set ; :: thesis: ( d is_min_depend PA,PB implies d in bool Y )
assume A6: d is_min_depend PA,PB ; :: thesis: d in bool Y
A7: d is_a_dependent_set_of PA by A6, Def2;
A8: ex A being set st
( A c= PA & A <> {} & d = union A ) by A7, Def1;
A9: d c= union PA by A8, ZFMISC_1:95;
thus d in bool Y by A1, A9; :: thesis: verum

end;

A10: ( d is_min_depend PA,PB implies ( d is_min_depend PA,PB & d in bool Y ) ) by A5;
thus ( d in X iff d is_min_depend PA,PB ) by A3, A10; :: thesis: verum

end;

take X ; :: thesis: ( X is Element of bool (bool Y) & X is a_partition of Y & ( for d being set holds
( d in X iff d is_min_depend PA,PB ) ) )
A11: Y c= union X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in union X )
assume A12: y in Y ; :: thesis: y in union X
consider a being Subset of Y such that
A13: y in a and
A14: a is_min_depend PA,PB by A12, Th13;
A15: a in X by A4, A14;
thus y in union X by A13, A15, TARSKI:def 4; :: thesis: verum

end;

A16: union X c= Y

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in union X or y in Y )
assume A17: y in union X ; :: thesis: y in Y
consider a being set such that
A18: y in a and
A19: a in X by A17, TARSKI:def 4;
A20: a is_min_depend PA,PB by A4, A19;
A21: a is_a_dependent_set_of PA by A20, Def2;
A22: ex A being set st
( A c= PA & A <> {} & a = union A ) by A21, Def1;
A23: a c= Y by A1, A22, ZFMISC_1:95;
thus y in Y by A18, A23; :: thesis: verum

end;

A24: union X = Y by A11, A16, XBOOLE_0:def 10;
A25: for A being Subset of Y st A in X holds
( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) )

proof

let A be Subset of Y; :: thesis: ( A in X implies ( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) ) )
assume A26: A in X ; :: thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) )
A27: A is_min_depend PA,PB by A4, A26;
A28: A is_a_dependent_set_of PA by A27, Def2;
A29: A is_a_dependent_set_of PB by A27, Def2;
consider Aa being set such that
A30: Aa c= PA and
A31: Aa <> {} and
A32: A = union Aa by A28, Def1;
consider aa being set such that
A33: aa in Aa by A31, XBOOLE_0:def 1;
A34: aa <> {} by A2, A30, A33;
A35: aa c= union Aa by A33, ZFMISC_1:92;
thus A <> {} by A32, A34, A35; :: thesis: for B being Subset of Y holds
( not B in X or A = B or A misses B )
let B be Subset of Y; :: thesis: ( not B in X or A = B or A misses B )
assume A36: B in X ; :: thesis: ( A = B or A misses B )
A37: B is_min_depend PA,PB by A4, A36;
A38: ( B is_a_dependent_set_of PA & B is_a_dependent_set_of PB ) by A37, Def2;

A39: now

assume A40: A meets B ; :: thesis: A = B
A41: ( A /\ B is_a_dependent_set_of PA & A /\ B is_a_dependent_set_of PB ) by A28, A29, A38, A40, Th11;
A42: A /\ B c= A by XBOOLE_1:17;
A43: A /\ B = A by A27, A41, A42, Def2;
A44: A c= B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )
assume A45: x in A ; :: thesis: x in B
thus x in B by A43, A45, XBOOLE_0:def 4; :: thesis: verum

end;

A46: A /\ B c= B by XBOOLE_1:17;
A47: A /\ B = B by A37, A41, A46, Def2;
A48: B c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in A )
assume A49: x in B ; :: thesis: x in A
thus x in A by A47, A49, XBOOLE_0:def 4; :: thesis: verum

end;

thus A = B by A44, A48, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( A = B or A misses B ) by A39; :: thesis: verum

end;

A50: X c= bool Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in bool Y )
assume A51: x in X ; :: thesis: x in bool Y
A52: x is_min_depend PA,PB by A4, A51;
A53: x is_a_dependent_set_of PA by A52, Def2;
A54: ex a being set st
( a c= PA & a <> {} & x = union a ) by A53, Def1;
A55: x c= Y by A1, A54, ZFMISC_1:95;
thus x in bool Y by A55; :: thesis: verum

end;

reconsider X = X as Subset-Family of Y by A50;
A56: X is a_partition of Y by A24, A25, EQREL_1:def 6;
thus ( X is Element of bool (bool Y) & X is a_partition of Y & ( for d being set holds
( d in X iff d is_min_depend PA,PB ) ) ) by A4, A56; :: thesis: verum