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