theorem :: CLASSES3:11

for X, Y being set holds
( Rrank X in Rrank Y or Rrank Y c= Rrank X )