for A being Ordinal holds the_rank_of A = A