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 ) ) ;
assume A c= B ; :: thesis: Rank A c= Rank B
then ( Rank A = Rank B or Rank A in Rank B ) by Th36, A1, ORDINAL1:11;
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;
hence contradiction by A2, ORDINAL1:5, Th36; :: thesis: verum