thus
( G <> {} implies ex X being a_partition of Y st

for x being set holds

( x in X iff x is_upper_min_depend_of G ) ) :: thesis: ( not G <> {} implies ex b_{1} being a_partition of Y st b_{1} = %I Y )_{1} being a_partition of Y st b_{1} = %I Y )
; :: thesis: verum

for x being set holds

( x in X iff x is_upper_min_depend_of G ) ) :: thesis: ( not G <> {} implies ex b

proof

thus
( not G <> {} implies ex b
defpred S_{1}[ set ] means $1 is_upper_min_depend_of G;

consider X being set such that

A1: for x being set holds

( x in X iff ( x in bool Y & S_{1}[x] ) )
from XFAMILY:sch 1();

A2: union X c= Y

for x being set holds

( x in X iff x is_upper_min_depend_of G )

then consider g being object such that

A6: g in G by XBOOLE_0:def 1;

reconsider g = g as a_partition of Y by A6, PARTIT1:def 3;

A7: union g = Y by EQREL_1:def 4;

A8: for x being set holds

( x in X iff x is_upper_min_depend_of G )

( A <> {} & ( for B being set holds

( not B in g or A = B or A misses B ) ) ) by EQREL_1:def 4;

A13: 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 in X iff x is_upper_min_depend_of G ) ) )

X c= bool Y by A1;

then reconsider X = X as Subset-Family of Y ;

X is a_partition of Y by A9, A13, A2, EQREL_1:def 4, XBOOLE_0:def 10;

hence ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds

( x in X iff x is_upper_min_depend_of G ) ) ) by A8; :: thesis: verum

end;consider X being set such that

A1: for x being set holds

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

A2: union X c= Y

proof

assume A5:
G <> {}
; :: thesis: ex X being a_partition of Y st
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

A3: y in a and

A4: a in X by TARSKI:def 4;

a in bool Y by A1, A4;

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

end;assume y in union X ; :: thesis: y in Y

then consider a being set such that

A3: y in a and

A4: a in X by TARSKI:def 4;

a in bool Y by A1, A4;

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

for x being set holds

( x in X iff x is_upper_min_depend_of G )

then consider g being object such that

A6: g in G by XBOOLE_0:def 1;

reconsider g = g as a_partition of Y by A6, PARTIT1:def 3;

A7: union g = Y by EQREL_1:def 4;

A8: for x being set holds

( x in X iff x is_upper_min_depend_of G )

proof

A9:
Y c= union X
let x be set ; :: thesis: ( x in X iff x is_upper_min_depend_of G )

for x being set st x is_upper_min_depend_of G holds

x in bool Y

end;for x being set st x is_upper_min_depend_of G holds

x in bool Y

proof

hence
( x in X iff x is_upper_min_depend_of G )
by A1; :: thesis: verum
let x be set ; :: thesis: ( x is_upper_min_depend_of G implies x in bool Y )

assume x is_upper_min_depend_of G ; :: thesis: x in bool Y

then ex A being set st

( A c= g & A <> {} & x = union A ) by A6, PARTIT1:def 1;

then x c= union g by ZFMISC_1:77;

hence x in bool Y by A7; :: thesis: verum

end;assume x is_upper_min_depend_of G ; :: thesis: x in bool Y

then ex A being set st

( A c= g & A <> {} & x = union A ) by A6, PARTIT1:def 1;

then x c= union g by ZFMISC_1:77;

hence x in bool Y by A7; :: thesis: verum

proof

A12:
for A being set st A in g holds
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 reconsider y = y as Element of Y ;

consider a being Subset of Y such that

A10: y in a and

A11: a is_upper_min_depend_of G by A5, Th2;

a in X by A8, A11;

hence y in union X by A10, TARSKI:def 4; :: thesis: verum

end;assume y in Y ; :: thesis: y in union X

then reconsider y = y as Element of Y ;

consider a being Subset of Y such that

A10: y in a and

A11: a is_upper_min_depend_of G by A5, Th2;

a in X by A8, A11;

hence y in union X by A10, TARSKI:def 4; :: thesis: verum

( A <> {} & ( for B being set holds

( not B in g or A = B or A misses B ) ) ) by EQREL_1:def 4;

A13: 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

take
X
; :: thesis: ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds
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 A14: A is_upper_min_depend_of G by A8;

then consider Aa being set such that

A15: Aa c= g and

A16: Aa <> {} and

A17: A = union Aa by A6, PARTIT1:def 1;

consider aa being object such that

A18: aa in Aa by A16, XBOOLE_0:def 1;

reconsider aa = aa as set by TARSKI:1;

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

aa <> {} by A12, A15, A18;

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_upper_min_depend_of G by A8;

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 A14: A is_upper_min_depend_of G by A8;

then consider Aa being set such that

A15: Aa c= g and

A16: Aa <> {} and

A17: A = union Aa by A6, PARTIT1:def 1;

consider aa being object such that

A18: aa in Aa by A16, XBOOLE_0:def 1;

reconsider aa = aa as set by TARSKI:1;

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

aa <> {} by A12, A15, A18;

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_upper_min_depend_of G by A8;

now :: thesis: ( A meets B implies A = B )

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

A22: for d being a_partition of Y st d in G holds

A /\ B is_a_dependent_set_of d

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

A25: A /\ B = A by A14, A22, XBOOLE_1:17;

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

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

end;A22: for d being a_partition of Y st d in G holds

A /\ B is_a_dependent_set_of d

proof

A23:
A /\ B = B
by A20, A22, XBOOLE_1:17;
let d be a_partition of Y; :: thesis: ( d in G implies A /\ B is_a_dependent_set_of d )

assume d in G ; :: thesis: A /\ B is_a_dependent_set_of d

then ( A is_a_dependent_set_of d & B is_a_dependent_set_of d ) by A14, A20;

hence A /\ B is_a_dependent_set_of d by A21, PARTIT1:9; :: thesis: verum

end;assume d in G ; :: thesis: A /\ B is_a_dependent_set_of d

then ( A is_a_dependent_set_of d & B is_a_dependent_set_of d ) by A14, A20;

hence A /\ B is_a_dependent_set_of d by A21, PARTIT1:9; :: thesis: verum

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

A25: A /\ B = A by A14, A22, XBOOLE_1:17;

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

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

( x in X iff x is_upper_min_depend_of G ) ) )

X c= bool Y by A1;

then reconsider X = X as Subset-Family of Y ;

X is a_partition of Y by A9, A13, A2, EQREL_1:def 4, XBOOLE_0:def 10;

hence ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds

( x in X iff x is_upper_min_depend_of G ) ) ) by A8; :: thesis: verum