let A, B be Ordinal; :: thesis: ( A c= B iff Rank A c= Rank B )
thus ( A c= B implies Rank A c= Rank B ) :: thesis: ( Rank A c= Rank B implies A c= B )

proof

A1: ( A c< B iff ( A c= B & A <> B ) ) by XBOOLE_0:def 8;
assume A2: A c= B ; :: thesis: Rank A c= Rank B
A3: ( A = B or A in B ) by A1, A2, ORDINAL1:21;
A4: ( Rank A = Rank B or Rank A in Rank B ) by A3, Th42;
thus Rank A c= Rank B by A4, ORDINAL1:def 2; :: thesis: verum

end;

assume that
A5: Rank A c= Rank B and
A6: not A c= B ; :: thesis: contradiction
A7: B in A by A6, ORDINAL1:26;
A8: Rank B in Rank A by A7, Th42;
thus contradiction by A5, A8, ORDINAL1:7; :: thesis: verum