let X be set ; :: thesis: for A being Ordinal holds
( X c= Rank A iff the_rank_of X c= A )
let A be Ordinal; :: thesis: ( X c= Rank A iff the_rank_of X c= A )
thus ( X c= Rank A implies the_rank_of X c= A ) by Def9; :: thesis: ( the_rank_of X c= A implies X c= Rank A )
assume the_rank_of X c= A ; :: thesis: X c= Rank A
then A1: Rank (the_rank_of X) c= Rank A by Th37;
X c= Rank (the_rank_of X) by Def9;
hence X c= Rank A by A1; :: thesis: verum