let X, Y be set ; :: thesis: ( X in Rrank Y implies Rrank X in Rrank Y )
assume X in Rrank Y ; :: thesis: Rrank X in Rrank Y
then the_rank_of X in the_rank_of Y by CLASSES1:66;
hence Rrank X in Rrank Y by CLASSES1:36; :: thesis: verum