theorem :: CLASSES2:43

for X, W being set st X is epsilon-transitive & X in Tarski-Class W holds
X in Rank (card (Tarski-Class W)) by Th42;