A1: ( union PA = Y & ( 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
A2: for d being set holds
( d in X iff ( d in bool Y & S₁[d] ) ) from XBOOLE_0:sch 1();
A3: 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 & d is_a_dependent_set_of PB & ( for x being set st x c= d & x is_a_dependent_set_of PA & x is_a_dependent_set_of PB holds
x = d ) ) by Def2;
then consider A being set such that
A4: ( A c= PA & A <> {} & d = union A ) by Def1;
d c= union PA by A4, ZFMISC_1:95;
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 A2; :: 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: union X = Y

proof

A6: 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 y in Y ; :: thesis: y in union X
then consider a being Subset of Y such that
A7: ( y in a & a is_min_depend PA,PB ) by Th13;
a in X by A3, A7;
hence y in union X by A7, TARSKI:def 4; :: thesis: verum

end;

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 y in union X ; :: thesis: y in Y
then consider a being set such that
A8: ( y in a & a in X ) by TARSKI:def 4;
a is_min_depend PA,PB by A3, A8;
then ( a is_a_dependent_set_of PA & a is_a_dependent_set_of PB & ( for d being set st d c= a & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = a ) ) by Def2;
then consider A being set such that
A9: ( A c= PA & A <> {} & a = union A ) by Def1;
a c= Y by A1, A9, ZFMISC_1:95;
hence y in Y by A8; :: thesis: verum

end;

hence union X = Y by A6, XBOOLE_0:def 10; :: thesis: verum

end;

A10: 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 A11: A is_min_depend PA,PB by A3;
then A12: ( A is_a_dependent_set_of PA & A is_a_dependent_set_of PB & ( for d being set st d c= A & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = A ) ) by Def2;
then consider Aa being set such that
A13: ( Aa c= PA & Aa <> {} & A = union Aa ) by Def1;
consider aa being set such that
A14: aa in Aa by A13, XBOOLE_0:def 1;
A15: aa <> {} by A1, A13, A14;
A16: aa c= union Aa by A14, ZFMISC_1:92;
ex ax being set st ax in aa by A15, XBOOLE_0:def 1;
hence A <> {} by A13, A16; :: 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 A17: B is_min_depend PA,PB by A3;
then A18: ( B is_a_dependent_set_of PA & B is_a_dependent_set_of PB & ( for d being set st d c= B & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = B ) ) by Def2;

now

assume A19: A meets B ; :: thesis: A = B
then A20: A /\ B is_a_dependent_set_of PA by A12, A18, Th11;
A21: A /\ B is_a_dependent_set_of PB by A12, A18, A19, Th11;
A /\ B c= A by XBOOLE_1:17;
then A22: A /\ B = A by A11, A20, A21, Def2;
A23: A c= B

proof

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

end;

A /\ B c= B by XBOOLE_1:17;
then A24: A /\ B = B by A17, A20, A21, Def2;
B c= A

proof

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

end;

hence A = B by A23, XBOOLE_0:def 10; :: thesis: verum

end;

hence ( A = B or A misses B ) ; :: thesis: verum

end;

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 x in X ; :: thesis: x in bool Y
then x is_min_depend PA,PB by A3;
then ( x is_a_dependent_set_of PA & x is_a_dependent_set_of PB & ( for d being set st d c= x & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = x ) ) by Def2;
then consider a being set such that
A25: ( a c= PA & a <> {} & x = union a ) by Def1;
x c= Y by A1, A25, ZFMISC_1:95;
hence x in bool Y ; :: thesis: verum

end;

then reconsider X = X as Subset-Family of Y ;
X is a_partition of Y by A5, A10, EQREL_1:def 6;
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 A3; :: thesis: verum