:: Zermelo Theorem and Axiom of Choice. The correspondence of well ordering relations and ordinal numbers :: by Grzegorz Bancerek :: :: Received June 26, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users
uniqueness
for b1, b2 being Relation st field b1= X & ( for Y, Z being set st Y in X & Z in X holds ( [Y,Z]in b1 iff Y c= Z ) ) & field b2= X & ( for Y, Z being set st Y in X & Z in X holds ( [Y,Z]in b2 iff Y c= Z ) ) holds b1= b2
for M being non emptyset 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 set st Choice /\ X ={x}