let M be non empty set ; :: thesis: ( ( for X being set st X in M holds
X <> {} ) & ( for X, Y being set st X in M & Y in M & X <> Y holds
X misses Y ) implies ex Choice being set st
for X being set st X in M holds
ex x being set st Choice /\ X = {x} )
assume that
A1: for X being set st X in M holds
X <> {} and
A2: for X, Y being set st X in M & Y in M & X <> Y holds
X misses Y ; :: thesis: ex Choice being set st
for X being set st X in M holds
ex x being set st Choice /\ X = {x}
consider R being Relation such that
A3: R well_orders union M by Th26;
A4: R is_antisymmetric_in union M by A3, WELLORD1:def 5;
A5: R is_well_founded_in union M by A3, WELLORD1:def 5;
A6: R is_connected_in union M by A3, WELLORD1:def 5;
A7: R is_reflexive_in union M by A3, WELLORD1:def 5;
defpred S₁[ set , set ] means ex X being set st
( $1 = X & $2 in X & ( for z being set st z in X holds
[$2,z] in R ) );
A8: for x, y, z being set st x in M & S₁[x,y] & S₁[x,z] holds
y = z

proof

let x, y, z be set ; :: thesis: ( x in M & S₁[x,y] & S₁[x,z] implies y = z )
assume A9: x in M ; :: thesis: ( not S₁[x,y] or not S₁[x,z] or y = z )
given Y being set such that A10: ( x = Y & y in Y & ( for u being set st u in Y holds
[y,u] in R ) ) ; :: thesis: ( not S₁[x,z] or y = z )
given Z being set such that A11: ( x = Z & z in Z & ( for u being set st u in Z holds
[z,u] in R ) ) ; :: thesis: y = z
( y in union M & z in union M & [y,z] in R & [z,y] in R ) by A9, A10, A11, TARSKI:def 4;
hence y = z by A4, RELAT_2:def 4; :: thesis: verum

end;

A12: for x being set st x in M holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in M implies ex y being set st S₁[x,y] )
assume x in M ; :: thesis: ex y being set st S₁[x,y]
then A13: ( x c= union M & x <> {} ) by A1, ZFMISC_1:92;
then consider y being set such that
A14: ( y in x & R -Seg y misses x ) by A5, WELLORD1:def 3;
take y ; :: thesis: S₁[x,y]
take x ; :: thesis: ( x = x & y in x & ( for z being set st z in x holds
[y,z] in R ) )
thus ( x = x & y in x ) by A14; :: thesis: for z being set st z in x holds
[y,z] in R
let z be set ; :: thesis: ( z in x implies [y,z] in R )
assume A15: z in x ; :: thesis: [y,z] in R
then A16: ( not y <> z or [y,z] in R or [z,y] in R ) by A6, A13, A14, RELAT_2:def 6;
not z in R -Seg y by A14, A15, XBOOLE_0:3;
hence [y,z] in R by A7, A13, A15, A16, RELAT_2:def 1, WELLORD1:def 1; :: thesis: verum

end;

consider f being Function such that
A17: ( dom f = M & ( for x being set st x in M holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(A8, A12);
take Choice = rng f; :: thesis: for X being set st X in M holds
ex x being set st Choice /\ X = {x}
let X be set ; :: thesis: ( X in M implies ex x being set st Choice /\ X = {x} )
assume A18: X in M ; :: thesis: ex x being set st Choice /\ X = {x}
take x = f . X; :: thesis: Choice /\ X = {x}
A19: for X being set st X in M holds
f . X in X

proof

let X be set ; :: thesis: ( X in M implies f . X in X )
assume X in M ; :: thesis: f . X in X
then ex Y being set st
( X = Y & f . X in Y & ( for z being set st z in Y holds
[(f . X),z] in R ) ) by A17;
hence f . X in X ; :: thesis: verum

end;

thus Choice /\ X c= {x} :: according to XBOOLE_0:def 10 :: thesis: {x} c= Choice /\ X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Choice /\ X or y in {x} )
assume y in Choice /\ X ; :: thesis: y in {x}
then A20: ( y in Choice & y in X ) by XBOOLE_0:def 4;
then consider z being set such that
A21: ( z in dom f & y = f . z ) by FUNCT_1:def 5;
assume not y in {x} ; :: thesis: contradiction
then X <> z by A21, TARSKI:def 1;
then X misses z by A2, A17, A18, A21;
then A22: X /\ z = {} by XBOOLE_0:def 7;
f . z in z by A17, A19, A21;
hence contradiction by A20, A21, A22, XBOOLE_0:def 4; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {x} or y in Choice /\ X )
assume y in {x} ; :: thesis: y in Choice /\ X
then y = x by TARSKI:def 1;
then ( y in Choice & y in X ) by A17, A18, A19, FUNCT_1:def 5;
hence y in Choice /\ X by XBOOLE_0:def 4; :: thesis: verum