theorem :: ORDERS_1:90

for M being non empty set st not {} in M holds
for Ch being Choice_Function of M holds Ch is Function of M,(union M) by Lm3;