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

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