theorem Th29: :: CLASSES2:29

for X, W being set st W is Tarski & W is epsilon-transitive & X in W holds
the_rank_of X in W