Theorem S.CO.1If x,y are sets and x:-y then !(y:-x).ProofAssume to the contrary that y:-x. Then we have x:-y and y:-x. Let z = {x,y}. By Axiom ZF9 we have \/(a:-z) a n z = O. But y :- x n {x,y} and x :- y n {x,y}. Contradiction. Thus !(y:-x).Theorem S.CO.2If x is a set then !(x:-x).ProofAssume that x:-x. Then by Theorem S.CO.1 !(x:-x). Contradiction.Definition S.CO.3 - OrdinalLet X be a set. We define that X is an ordinal if and only if (1) /\(x,y:-X) x:-y or y:-x or x = y, (2) /\(x,y,z:-X) (x:-y and y:-z) => x:-z, (3) /\(x:-X) x c X.Theorem S.CO.4If x is an ordinal, y c x and y != O then \/(e:-y)/\(z:-y) e:-z or e = z.ProofBy Axiom ZF9 we have e:-y such that e n y = O. Take any z:-y. Since e n y = O, !(z:-e). Since x is an ordinal, e:-z or e = z. We have proved that \/(e:-y)/\(z:-y) e:-z or e = z.Theorem S.CO.5If x is an ordinal, a,b:-x and a:-b then a c b.ProofTake any a,b:-x such that a:-b. Take any t:-a. By Definition S.CO.3 t:-b. Thus a c b.Theorem S.CO.6If x is an ordinal and y:-x then y is an ordinal.ProofBy Definition S.CO.3 y c x. Hence /\(p,q:-y) p:-q or q:-p or p = q, /\(p,q,r:-y) (p:-q and q:-r) => p:-r. We have to show that /\(z:-y) z c y. Take any z:-y. Since y c x, z:-x. Now we have z,y:-x and z:-y. By Theorem S.CO.5 z c y. We have proved that y is an ordinal.Theorem S.CO.7If x is an ordinal and a,b:-x then a c b <=> a:-b or a = b.ProofBy Theorem S.CO.5 it is enough to show that a c b => a:-b or a = b. Assume that a c b. Assume to the contrary that !(a:-b) and a != b. Since x is an ordinal b:-a. Then by Theorem S.CO.5 b c a. Hence a = b. Contradiction. We have shown that a c b => a:-b or a = b.Theorem S.CO.8If X is an ordinal and E = {(a,b):-XxX | a c b} then (X,E) is a well ordered set.ProofBy Theorem S.CO.7, Theorem S.CO.4 and Definition S.CO.3.Remark:If we write that (X,c) is a well ordered set we mean that (X,E) with E = {(a,b):-XxX | a c b} is a well ordered set.Theorem S.CO.9If x and y are ordinals then (x n y) is an initial segment of x in (x,c).ProofTake any a :- x n y. Take any t:-x such that t c a. We will show that t :- x n y. By Theorem S.CO.7 t = a or t:-a. If a = t there is no problem. Assume that t:-a. Since x,y are ordinals, a c x n y. Then t :- x n y. Thus x n y is an initial segment of x in (x,c).Theorem S.CO.10If x and y are ordinals then x c y or y c x.ProofAssume to the contrary that !(x c y) and !(y c x). Then x n y != x and x n y != y. By Theorem S.CO.9 x n y is an initial segment of x in (x,c). Recall that x n y != x, By Theorem S.O.8 we have r:-x such that x n y = {z:-x | z c r and z!=r} = {z:-x|z:-r}. Since x is an ordinal, r c x. Hence r = x n r = x n y. By Theorem S.CO.9 x n y is an initial segment of y in (y,c). Recall that x n y != y, By Theorem S.O.8 we have s:-y such that x n y = {z:-y | z c s and z!=s} = {z:-y|z:-s}. Since y is an ordinal, s c y. Hence s = s n y = x n y. Thus s = r. Since r:-x and s:-y, r:-x n y. Then r:-r. Contradiction.Theorem S.CO.11If x and y are ordinals then x:-y or y:-x or y = x.ProofBy Theorem S.CO.10 we can assume that x c y. Then by Theorem S.CO.9 x is an initial segment of y. If x = y there is no problem. Assume that x != y. Now by Theorem S.O.8 we have r:-y such that x = {z:-y|z:-r}. Since y is an ordinal r c y. Hence x = y n r = r. Thus x:-y.Theorem S.CO.12If x,y are ordinals then x:-y <=> x c y and x != y.ProofAssume that x c y and x != y. By Theorem S.CO.11 x:-y or y:-x or x = y. If y:-x then y:-y because x c y. Then contradiction. Thus x:-y. Assume that x:-y. By Theorem S.CO.2 y != x. By Theorem S.CO.10 we have x c y or y c x. If y c x then x:-x because x:-y. Then contradiction. Thus x c y.Theorem S.CO.13If x,y,z are ordinals and x:-y and y:-z then x:-z.ProofBy S.CO.11 we have x c z and y c z. Hence x c z. If x = z then x:-y and y:-x. Then contradiction. Hence x != z. Thus By S.CO.11 x:-z.Theorem S.CO.14If y is a set such that /\(x:-y) x is an ordinal then \/(e:-y)/\(z:-y) e:-z or e = z.ProofBy Axiom ZF9 we have e:-y such that e n y = O. Take any z:-y. Since e n y = O, !(z:-e). Since z,e are ordinals, e:-z or e = z. We have proved that \/(e:-y)/\(z:-y) e:-z or e = z.Theorem S.CO.15If y is a set, /\(x:-y) ((x is an ordinal) and x c y) then y is an ordinal.ProofBy Theorem S.CO.11, Theorem S.CO.13 and Definition S.CO.3.