let X, Y be set ; :: thesis: ( Rrank X in Rrank Y or Rrank Y c= Rrank X )
assume not Rrank X in Rrank Y ; :: thesis: Rrank Y c= Rrank X
then not the_rank_of X in the_rank_of Y by CLASSES1:36;
hence Rrank Y c= Rrank X by CLASSES1:37, ORDINAL1:16; :: thesis: verum