Zermelo Theorem and Axiom of Choice. The correspondence of well ordering relations and ordinal numbers (original) (raw)

let X be set ;

func RelIncl X -> Relation means :Def1: :: WELLORD2:def 1
( field it = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in it iff Y c= Z ) ) );

existence
ex b1 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 ) ) )

proof end;

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

proof end;