theorem Th68: :: CLASSES1:68

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