let X, Y be set ; :: thesis: ( X c= Y implies the_rank_of X c= the_rank_of Y )
assume A1: X c= Y ; :: thesis: the_rank_of X c= the_rank_of Y
Y c= Rank (the_rank_of Y) by Def9;
then X c= Rank (the_rank_of Y) by A1;
hence the_rank_of X c= the_rank_of Y by Def9; :: thesis: verum