theorem :: CLASSES1:67

for X, Y being set st X c= Y holds
the_rank_of X c= the_rank_of Y