let M be non empty set ; :: thesis: ( ( for X being set st X in M holds
X <> {} ) implies ex Choice being Function st
( dom Choice = M & ( for X being set st X in M holds
Choice . X in X ) ) )
assume A1: for X being set st X in M holds
X <> {} ; :: thesis: ex Choice being Function st
( dom Choice = M & ( for X being set st X in M holds
Choice . X in X ) )
consider R being Relation such that
A2: R well_orders union M by Th26;
defpred S₁[ set , set ] means ( $2 in $1 & ( for z being set st z in $1 holds
[$2,z] in R ) );
A3: R is_connected_in union M by A2, WELLORD1:def 5;
A4: R is_reflexive_in union M by A2, WELLORD1:def 5;
A5: R is_well_founded_in union M by A2, WELLORD1:def 5;
A6: 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 A7: x in M ; :: thesis: ex y being set st S₁[x,y]
then A8: x c= union M by ZFMISC_1:92;
x <> {} by A1, A7;
then consider y being set such that
A9: y in x and
A10: R -Seg y misses x by A5, A8, WELLORD1:def 3;
take y ; :: thesis: S₁[x,y]
thus y in x by A9; :: 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 A11: z in x ; :: thesis: [y,z] in R
(R -Seg y) /\ x = {} by A10, XBOOLE_0:def 7;
then A12: not z in R -Seg y by A11, XBOOLE_0:def 4;
( not y <> z or [y,z] in R or [z,y] in R ) by A3, A8, A9, A11, RELAT_2:def 6;
hence [y,z] in R by A4, A8, A11, A12, RELAT_2:def 1, WELLORD1:def 1; :: thesis: verum

end;

A13: R is_antisymmetric_in union M by A2, WELLORD1:def 5;
A14: 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 A15: x in M ; :: thesis: ( not S₁[x,y] or not S₁[x,z] or y = z )
assume that
A16: y in x and
A17: for u being set st u in x holds
[y,u] in R ; :: thesis: ( not S₁[x,z] or y = z )
A18: y in union M by A15, A16, TARSKI:def 4;
assume that
A19: z in x and
A20: for u being set st u in x holds
[z,u] in R ; :: thesis: y = z
A21: z in union M by A15, A19, TARSKI:def 4;
( [y,z] in R & [z,y] in R ) by A16, A17, A19, A20;
hence y = z by A13, A18, A21, RELAT_2:def 4; :: thesis: verum

end;

consider f being Function such that
A22: ( dom f = M & ( for x being set st x in M holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(A14, A6);
take f ; :: thesis: ( dom f = M & ( for X being set st X in M holds
f . X in X ) )
thus ( dom f = M & ( for X being set st X in M holds
f . X in X ) ) by A22; :: thesis: verum