theorem :: CLASSES2:37

for X, W being set holds
( not X c= Rank (card (Tarski-Class W)) or X, Rank (card (Tarski-Class W)) are_equipotent or X in Rank (card (Tarski-Class W)) ) by Th36;