let X, Y be set ; :: thesis: ( X c= Rrank Y implies Rrank X c= Rrank Y )
assume X c= Rrank Y ; :: thesis: Rrank X c= Rrank Y
then the_rank_of X c= the_rank_of Y by CLASSES1:65;
hence Rrank X c= Rrank Y by CLASSES1:37; :: thesis: verum