theorem :: CLASSES3:7

for X being set holds X c= Rrank X by CLASSES1:def 9;