let A be Ordinal; :: thesis: the_rank_of (Rank A) = A
for B being Ordinal st Rank A c= Rank B holds
A c= B by Th37;
hence the_rank_of (Rank A) = A by Def9; :: thesis: verum