theorem :: CLASSES1:73

for A being Ordinal holds the_rank_of A = A