theorem :: CLASSES1:20
for X being set ex A being Ordinal st
( Tarski-Class (X,A) = Tarski-Class X & ( for B being Ordinal st B in A holds
Tarski-Class (X,B) <> Tarski-Class X ) )