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 A c= B ; :: thesis: Rank A c= Rank B
then ( A = B or A in B ) by A1, ORDINAL1:21;
then ( Rank A = Rank B or Rank A in Rank B ) by Th42;
hence Rank A c= Rank B by ORDINAL1:def 2; :: thesis: verum

end;

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