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 :: thesis: for A, B being Ordinal holds S₂[B]

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 :: thesis: ( ex C being Ordinal st B = succ C implies Rank A in Rank B )

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:6;

now :: thesis: ( not A in C implies Rank A = Rank C )

assume A8: not A in C ; :: thesis: Rank A = Rank C
( ( A c= C & A <> C ) iff A c< C ) ;
hence Rank A = Rank C by A4, A6, A8, ORDINAL1:11, ORDINAL1:22; :: thesis: verum

end;

then Rank A c= Rank C by A7, ORDINAL1:def 2;
hence Rank A in Rank B by A6, Th32; :: thesis: verum

end;

now :: thesis: ( ( for C being Ordinal holds B <> succ C ) implies Rank A in Rank B )

assume A9: for C being Ordinal holds B <> succ C ; :: thesis: Rank A in Rank B
then A10: B is limit_ordinal by ORDINAL1:29;
A11: B <> succ A by A9;
succ A c< B by A11, A4, ORDINAL1:21;
then A12: succ A in B by ORDINAL1:11;
Rank A in Rank (succ A) by Th32;
hence Rank A in Rank B by A10, A12, Th31; :: thesis: verum

end;

hence Rank A in Rank B by A5; :: thesis: verum

end;

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

end;

hence S₁[A,B] ; :: thesis: ( Rank A in Rank B implies A in B )
assume that
A13: Rank A in Rank B and
A14: not A in B ; :: thesis: contradiction
( B in A or B = A ) by A14, ORDINAL1:14;
hence contradiction by A1, A13; :: thesis: verum