theorem Th30: :: CLASSES2:30

for W being set st W is Tarski & W is epsilon-transitive holds
W c= Rank (card W)