theorem Th36: :: CLASSES2:36

for X, W being set st W is Tarski & X c= Rank (card W) & not X, Rank (card W) are_equipotent holds
X in Rank (card W)