theorem :: CLASSES1:64

for A being Ordinal holds the_rank_of (Rank A) = A