A1: union PA = Y by EQREL_1:def 4;
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 4;
defpred S1[ 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 & S1[d] ) ) from 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 )
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 d is_min_depend PA,PB ; :: thesis: d in bool Y
then d is_a_dependent_set_of PA ;
then ex A being set st
( A c= PA & A <> {} & d = union A ) ;
then d c= union PA by ZFMISC_1:77;
hence d in bool Y by A1; :: thesis: verum
end;
then ( d is_min_depend PA,PB implies ( d is_min_depend PA,PB & d in bool Y ) ) ;
hence ( d in X iff d is_min_depend PA,PB ) by A3; :: 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 ) ) )

A5: Y c= union X
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in union X )
assume y in Y ; :: thesis: y in union X
then consider a being Subset of Y such that
A6: y in a and
A7: a is_min_depend PA,PB by Th11;
a in X by A4, A7;
hence y in union X by ; :: thesis: verum
end;
union X c= Y
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in union X or y in Y )
assume y in union X ; :: thesis: y in Y
then consider a being set such that
A8: y in a and
A9: a in X by TARSKI:def 4;
a is_min_depend PA,PB by A4, A9;
then a is_a_dependent_set_of PA ;
then ex A being set st
( A c= PA & A <> {} & a = union A ) ;
then a c= Y by ;
hence y in Y by A8; :: thesis: verum
end;
then A10: union X = Y by ;
A11: 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 A in X ; :: thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) )

then A12: A is_min_depend PA,PB by A4;
then A13: A is_a_dependent_set_of PA ;
A14: A is_a_dependent_set_of PB by A12;
consider Aa being set such that
A15: Aa c= PA and
A16: Aa <> {} and
A17: A = union Aa by A13;
consider aa being object such that
A18: aa in Aa by ;
A19: aa <> {} by A2, A15, A18;
reconsider aa = aa as set by TARSKI:1;
aa c= union Aa by ;
hence A <> {} by ; :: 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 B in X ; :: thesis: ( A = B or A misses B )
then A20: B is_min_depend PA,PB by A4;
then A21: ( B is_a_dependent_set_of PA & B is_a_dependent_set_of PB ) ;
now :: thesis: ( A meets B implies A = B )end;
hence ( A = B or A misses B ) ; :: thesis: verum
end;
X c= bool Y
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in bool Y )
reconsider xx = x as set by TARSKI:1;
assume x in X ; :: thesis: x in bool Y
then xx is_min_depend PA,PB by A4;
then xx is_a_dependent_set_of PA ;
then ex a being set st
( a c= PA & a <> {} & x = union a ) ;
then xx c= Y by ;
hence x in bool Y ; :: thesis: verum
end;
then reconsider X = X as Subset-Family of Y ;
X is a_partition of Y by ;
hence ( 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; :: thesis: verum