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_reflexive_in union M by A3, WELLORD1:def 5;
A5: R is_connected_in union M by A3, WELLORD1:def 5;
defpred S₁[ set , set ] means ( $2 in $1 & ( for z being set st z in $1 holds
[$2,z] in R ) );
A6: R is_antisymmetric_in union M by A3, WELLORD1:def 5;
A7: 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 A8: x in M ; :: thesis: ( not S₁[x,y] or not S₁[x,z] or y = z )
assume that
A9: y in x and
A10: for u being set st u in x holds
[y,u] in R ; :: thesis: ( not S₁[x,z] or y = z )
A11: y in union M by A8, A9, TARSKI:def 4;
assume that
A12: z in x and
A13: for u being set st u in x holds
[z,u] in R ; :: thesis: y = z
A14: z in union M by A8, A12, TARSKI:def 4;
( [y,z] in R & [z,y] in R ) by A9, A10, A12, A13;
hence y = z by A6, A11, A14, RELAT_2:def 4; :: thesis: verum

end;

A15: R is_well_founded_in union M by A3, WELLORD1:def 5;
A16: 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 A17: x in M ; :: thesis: ex y being set st S₁[x,y]
then A18: x c= union M by ZFMISC_1:74;
x <> {} by A1, A17;
then consider y being set such that
A19: y in x and
A20: R -Seg y misses x by A15, A18, WELLORD1:def 3;
take y ; :: thesis: S₁[x,y]
thus y in x by A19; :: 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 A21: z in x ; :: thesis: [y,z] in R
then A22: not z in R -Seg y by A20, XBOOLE_0:3;
( not y <> z or [y,z] in R or [z,y] in R ) by A5, A18, A19, A21, RELAT_2:def 6;
hence [y,z] in R by A4, A18, A21, A22, RELAT_2:def 1, WELLORD1:1; :: thesis: verum

end;

consider f being Function such that
A23: ( dom f = M & ( for x being set st x in M holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(A7, A16);
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 A24: X in M ; :: thesis: ex x being set st Choice /\ X = {x}
take x = f . X; :: thesis: Choice /\ X = {x}
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 A25: y in Choice /\ X ; :: thesis: y in {x}
then A26: y in X by XBOOLE_0:def 4;
y in Choice by A25, XBOOLE_0:def 4;
then consider z being set such that
A27: z in dom f and
A28: y = f . z by FUNCT_1:def 3;
assume not y in {x} ; :: thesis: contradiction
then X <> z by A28, TARSKI:def 1;
then X misses z by A2, A23, A24, A27;
then A29: X /\ z = {} by XBOOLE_0:def 7;
f . z in z by A23, A27;
hence contradiction by A26, A28, A29, 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 A30: y = x by TARSKI:def 1;
then A31: y in X by A24, A23;
y in Choice by A23, A24, A30, FUNCT_1:def 3;
hence y in Choice /\ X by A31, XBOOLE_0:def 4; :: thesis: verum