let A be Ordinal; :: thesis: the_rank_of (Rank A) = A
A1: for B being Ordinal st Rank A c= Rank B holds
A c= B by Th43;
thus the_rank_of (Rank A) = A by A1, Def8; :: thesis: verum