theorem :: WELLORD2:18

for M being non empty set st ( for X being set st X in M holds
X <> {} ) & ( for X, Y being set st X in M & Y in M & X <> Y holds
X misses Y ) holds
ex Choice being set st
for X being set st X in M holds
ex x being object st Choice /\ X = {x}