let A, B be Ordinal; :: thesis: ( A in B iff Rank A in Rank B )
defpred S₁[ Ordinal, Ordinal] means ( $1 in $2 implies Rank $1 in Rank $2 );

A1: now

let A be Ordinal; :: thesis: for B being Ordinal holds S₂[B]
defpred S₂[ Ordinal] means S₁[A,$1];
A2: for B being Ordinal st ( for C being Ordinal st C in B holds
S₂[C] ) holds
S₂[B]

proof

let B be Ordinal; :: thesis: ( ( for C being Ordinal st C in B holds
S₂[C] ) implies S₂[B] )
assume that
A3: for C being Ordinal st C in B holds
S₁[A,C] and
A4: A in B ; :: thesis: Rank A in Rank B

A5: now

given C being Ordinal such that A6: B = succ C ; :: thesis: Rank A in Rank B
A7: ( A in C implies Rank A in Rank C ) by A3, A6, ORDINAL1:10;

A8: now

assume A9: not A in C ; :: thesis: Rank A = Rank C
A10: ( ( A c= C & A <> C ) iff A c< C ) by XBOOLE_0:def 8;
thus Rank A = Rank C by A4, A6, A9, A10, ORDINAL1:21, ORDINAL1:34; :: thesis: verum

end;

A11: Rank A c= Rank C by A7, A8, ORDINAL1:def 2;
thus Rank A in Rank B by A6, A11, Th36; :: thesis: verum

end;

A12: now

assume A13: for C being Ordinal holds B <> succ C ; :: thesis: Rank A in Rank B
A14: B is limit_ordinal by A13, ORDINAL1:42;
A15: B <> succ A by A13;
A16: succ A c= B by A4, ORDINAL1:33;
A17: succ A c< B by A15, A16, XBOOLE_0:def 8;
A18: succ A in B by A17, ORDINAL1:21;
A19: Rank A in Rank (succ A) by Th36;
thus Rank A in Rank B by A14, A18, A19, Th35; :: thesis: verum

end;

thus Rank A in Rank B by A5, A12; :: thesis: verum

end;

thus for B being Ordinal holds S₂[B] from ORDINAL1:sch 2(A2); :: thesis: verum

end;

thus S₁[A,B] by A1; :: thesis: ( Rank A in Rank B implies A in B )
assume that
A20: Rank A in Rank B and
A21: not A in B ; :: thesis: contradiction
A22: ( B in A or B = A ) by A21, ORDINAL1:24;
thus contradiction by A1, A20, A22; :: thesis: verum