let X, Y be set ; ( 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
; 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;
then consider B being Ordinal such that
A7:
A = succ B
by ORDINAL1:29;
take
B
; ( 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; verum