theorem Th40: :: CLASSES2:40

for A being Ordinal
for X being set st X is epsilon-transitive & A in the_rank_of X holds
ex Y being set st
( Y in X & the_rank_of Y = A )