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