theorem :: CLASSES3:9

for X, Y being set st X in Rrank Y holds
Rrank X in Rrank Y