theorem :: CLASSES1:12

for X, Y being set
for A being Ordinal st Y in Tarski-Class (X,A) holds
bool Y in Tarski-Class (X,(succ A)) by Th10;