theorem Th46: :: CLASSES1:46

for X being set
for A being Ordinal st X is epsilon-transitive & (Rank A) /\ (Tarski-Class X) = (Rank (succ A)) /\ (Tarski-Class X) holds
Tarski-Class X c= Rank A