let M be non empty set ; :: thesis: ( not {} in M implies for Ch being Choice_Function of M
for X being set st X in M holds
Ch . X in X )
assume A1: not {} in M ; :: thesis: for Ch being Choice_Function of M
for X being set st X in M holds
Ch . X in X
let Ch be Choice_Function of M; :: thesis: for X being set st X in M holds
Ch . X in X
let X be set ; :: thesis: ( X in M implies Ch . X in X )
assume A2: X in M ; :: thesis: Ch . X in X
then A3: X <> {} by A1;
A4: (id M) . X = X by A2, FUNCT_1:18;
X in dom Ch by A2, PARTFUN1:def 2;
then Ch . X = the Element of (id M) . X by Def2
.= the Element of X by A4 ;
hence Ch . X in X by A3; :: thesis: verum