theorem Th42: :: CLASSES2:42

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