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;
A3: ex A being Ordinal st Tarski-Class X,A = Tarski-Class X by Th22;
A4: ex A being Ordinal st S₁[A] by A2, A3;
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;

A8: now

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

end;

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