theorem :: CLASSES1:21

for X, Y being set st Y <> X & Y in Tarski-Class X holds
ex A being Ordinal st
( not Y in Tarski-Class (X,A) & Y in Tarski-Class (X,(succ A)) )