theorem Th31: :: CLASSES2:31
for W being set st W is Tarski & W is epsilon-transitive holds
Rank (card W) = W by Th27, Th30;