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 S_{1}[ 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_{1}[d] ) )
from XFAMILY:sch 1();

A4: for d being set holds

( d in X iff d is_min_depend PA,PB )

( d in X iff d is_min_depend PA,PB ) ) )

A5: Y c= union X

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 ) ) )

X is a_partition of Y by A10, A11, EQREL_1:def 4;

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

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 S

consider X being set such that

A3: for d being set holds

( d in X iff ( d in bool Y & S

A4: for d being set holds

( d in X iff d is_min_depend PA,PB )

proof

take
X
; :: thesis: ( X is Element of bool (bool Y) & X is a_partition of Y & ( for d being set holds
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

hence ( d in X iff d is_min_depend PA,PB ) by A3; :: thesis: verum

end;for d being set st d is_min_depend PA,PB holds

d in bool Y

proof

then
( d is_min_depend PA,PB implies ( d is_min_depend PA,PB & d in bool Y ) )
;
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;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

hence ( d in X iff d is_min_depend PA,PB ) by A3; :: thesis: verum

( d in X iff d is_min_depend PA,PB ) ) )

A5: Y c= union X

proof

union X c= Y
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 A6, TARSKI:def 4; :: thesis: verum

end;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 A6, TARSKI:def 4; :: thesis: verum

proof

then A10:
union X = Y
by A5, XBOOLE_0:def 10;
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 A1, ZFMISC_1:77;

hence y in Y by A8; :: thesis: verum

end;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 A1, ZFMISC_1:77;

hence y in Y by A8; :: thesis: verum

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

X c= bool Y
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 A16, XBOOLE_0:def 1;

A19: aa <> {} by A2, A15, A18;

reconsider aa = aa as set by TARSKI:1;

aa c= union Aa by A18, ZFMISC_1:74;

hence A <> {} by A17, A19; :: 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 ) ;

end;( 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 A16, XBOOLE_0:def 1;

A19: aa <> {} by A2, A15, A18;

reconsider aa = aa as set by TARSKI:1;

aa c= union Aa by A18, ZFMISC_1:74;

hence A <> {} by A17, A19; :: 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 )

hence
( A = B or A misses B )
; :: thesis: verumassume
A meets B
; :: thesis: A = B

then A22: ( A /\ B is_a_dependent_set_of PA & A /\ B is_a_dependent_set_of PB ) by A13, A14, A21, Th9;

A /\ B c= A by XBOOLE_1:17;

then A23: A /\ B = A by A12, A22;

A24: A c= B by A23, XBOOLE_0:def 4;

A /\ B c= B by XBOOLE_1:17;

then A25: A /\ B = B by A20, A22;

B c= A by A25, XBOOLE_0:def 4;

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

end;then A22: ( A /\ B is_a_dependent_set_of PA & A /\ B is_a_dependent_set_of PB ) by A13, A14, A21, Th9;

A /\ B c= A by XBOOLE_1:17;

then A23: A /\ B = A by A12, A22;

A24: A c= B by A23, XBOOLE_0:def 4;

A /\ B c= B by XBOOLE_1:17;

then A25: A /\ B = B by A20, A22;

B c= A by A25, XBOOLE_0:def 4;

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

proof

then reconsider X = X as Subset-Family of Y ;
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 A1, ZFMISC_1:77;

hence x in bool Y ; :: thesis: verum

end;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 A1, ZFMISC_1:77;

hence x in bool Y ; :: thesis: verum

X is a_partition of Y by A10, A11, EQREL_1:def 4;

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