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 )
consider x being Element of M;
A1: x in M ;
assume not {} in M ; :: thesis: dom CF = M
then union M <> {} by A1, ORDERS_1:91;
hence dom CF = M by FUNCT_2:def 1; :: thesis: verum