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