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₁ being a_partition of Y st b₁ = %I Y )

proof

defpred S₁[ 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₁[x] ) ) from XBOOLE_0:sch 1();
A2: 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
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 A5: G <> {} ; :: thesis: ex X being a_partition of Y st
for x being set holds
( x in X iff x is_upper_min_depend_of G )
then consider g being set 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 6;
A8: for x being set holds
( x in X iff x is_upper_min_depend_of G )

proof

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

proof

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 x is_a_dependent_set_of g by A6, Def2;
then ex A being set st
( A c= g & A <> {} & x = union A ) by PARTIT1:def 1;
then x c= union g by ZFMISC_1:95;
hence x in bool Y by A7; :: thesis: verum

end;

then ( x is_upper_min_depend_of G implies ( x is_upper_min_depend_of G & x in bool Y ) ) ;
hence ( x in X iff x is_upper_min_depend_of G ) by A1; :: thesis: verum

end;

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 reconsider y = y as Element of Y ;
consider a being Subset of Y such that
A9: y in a and
A10: a is_upper_min_depend_of G by A5, Th2;
a in X by A8, A10;
hence y in union X by A9, TARSKI:def 4; :: thesis: verum

end;

then A11: Y = union X by A2, XBOOLE_0:def 10;
A12: for A being set st A in g holds
( A <> {} & ( for B being set holds
( not B in g or A = B or A misses B ) ) ) by EQREL_1:def 6;
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

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 A is_a_dependent_set_of g by A6, Def2;
then consider Aa being set such that
A15: Aa c= g and
A16: Aa <> {} and
A17: A = union Aa by PARTIT1:def 1;
consider aa being set such that
A18: aa in Aa by A16, XBOOLE_0:def 1;
A19: aa c= union Aa by A18, ZFMISC_1:92;
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

assume 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

proof

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, Def2;
hence A /\ B is_a_dependent_set_of d by A21, PARTIT1:11; :: thesis: verum

end;

A /\ B c= B by XBOOLE_1:17;
then A23: A /\ B = B by A20, A22, Def2;
A24: 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 A23, XBOOLE_0:def 4; :: thesis: verum

end;

A /\ B c= A by XBOOLE_1:17;
then A25: A /\ B = A by A14, A22, Def2;
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 A25, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

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

end;

take X ; :: thesis: ( 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 ) ) )
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
hence x in bool Y by A1; :: thesis: verum

end;

then reconsider X = X as Subset-Family of Y ;
X is a_partition of Y by A11, A13, EQREL_1:def 6;
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;

thus ( not G <> {} implies ex b₁ being a_partition of Y st b₁ = %I Y ) ; :: thesis: verum