let X, Y be set ; :: thesis: ( Y <> X & Y in Tarski-Class X implies ex A being Ordinal st
( not Y in Tarski-Class (X,A) & Y in Tarski-Class (X,(succ A)) ) )
assume that
A1: Y <> X and
A2: Y in Tarski-Class X ; :: thesis: ex A being Ordinal st
( not Y in Tarski-Class (X,A) & Y in Tarski-Class (X,(succ A)) )
defpred S1[ Ordinal] means Y in Tarski-Class (X,$1);
ex A being Ordinal st Tarski-Class (X,A) = Tarski-Class X by Th19;
then A3: ex A being Ordinal st S1[A] by A2;
consider A being Ordinal such that
A4: ( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch 1(A3);
 A5: not Y in {X} by A1, TARSKI:def 1;
A6: Tarski-Class (X,{}) = {X} by Lm1;
now :: thesis: not A is limit_ordinal
assume A is limit_ordinal ; :: thesis: contradiction
then ex B being Ordinal st
( B in A & Y in Tarski-Class (X,B) ) by A4, A5, A6, Th13;
hence contradiction by A4, ORDINAL1:5; :: thesis: verum
end;
then consider B being Ordinal such that
A7: A = succ B by ORDINAL1:29;
take B ; :: thesis: ( not Y in Tarski-Class (X,B) & Y in Tarski-Class (X,(succ B)) )
not A c= B by A7, ORDINAL1:5, ORDINAL1:6;
hence ( not Y in Tarski-Class (X,B) & Y in Tarski-Class (X,(succ B)) ) by A4, A7; :: thesis: verum