let Y, X 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 A1: ( Y <> X & 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 S₁[ Ordinal] means Y in Tarski-Class X,$1;
ex A being Ordinal st Tarski-Class X,A = Tarski-Class X by Th22;
then A2: ex A being Ordinal st S₁[A] by A1;
consider A being Ordinal such that
A3: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A2);
A4: ( not Y in {X} & Tarski-Class X,{} = {X} ) by A1, Lm1, TARSKI:def 1;

now

assume A is limit_ordinal ; :: thesis: contradiction
then ex B being Ordinal st
( B in A & Y in Tarski-Class X,B ) by A3, A4, Th16;
hence contradiction by A3, ORDINAL1:7; :: thesis: verum

end;

then consider B being Ordinal such that
A5: A = succ B by ORDINAL1:42;
take B ; :: thesis: ( not Y in Tarski-Class X,B & Y in Tarski-Class X,(succ B) )
not A c= B by A5, ORDINAL1:7, ORDINAL1:10;
hence ( not Y in Tarski-Class X,B & Y in Tarski-Class X,(succ B) ) by A3, A5; :: thesis: verum