for M being non empty set st not {} in M holds
for Ch being Choice_Function of M
for X being set st X in M holds
Ch . X in X by Lm2;