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