let M be non empty set ; :: thesis: for CF being Choice_Function of M st not {} in M holds

dom CF = M

let CF be Choice_Function of M; :: thesis: ( not {} in M implies dom CF = M )

set x = the Element of M;

A1: the Element of M in M ;

assume A2: not {} in M ; :: thesis: dom CF = M

then A3: CF is Function of M,(union M) by ORDERS_1:90;

union M <> {} by A1, ORDERS_1:6, A2;

hence dom CF = M by FUNCT_2:def 1, A3; :: thesis: verum

dom CF = M

let CF be Choice_Function of M; :: thesis: ( not {} in M implies dom CF = M )

set x = the Element of M;

A1: the Element of M in M ;

assume A2: not {} in M ; :: thesis: dom CF = M

then A3: CF is Function of M,(union M) by ORDERS_1:90;

union M <> {} by A1, ORDERS_1:6, A2;

hence dom CF = M by FUNCT_2:def 1, A3; :: thesis: verum