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

now

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

end;

then consider B being Ordinal such that
A11: 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 A11, ORDINAL1:7, ORDINAL1:10;
hence ( not Y in Tarski-Class X,B & Y in Tarski-Class X,(succ B) ) by A5, A11; :: thesis: verum