theorem Th18: :: CLASSES1:18

for X being set
for A being Ordinal st Tarski-Class (X,A) = Tarski-Class (X,(succ A)) holds
Tarski-Class (X,A) = Tarski-Class X