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:11;
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
A2: Rank A c= Rank B and
A3: not A c= B ; :: thesis: contradiction
B in A by A3, ORDINAL1:16;
then Rank B in Rank A by Th42;
hence contradiction by A2, ORDINAL1:5; :: thesis: verum