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
A2: Y c= Rank (the_rank_of Y) by Def8;
A3: X c= Rank (the_rank_of Y) by A1, A2, XBOOLE_1:1;
thus the_rank_of X c= the_rank_of Y by A3, Def8; :: thesis: verum