let X be set ; :: thesis: ex A being Ordinal st Tarski-Class X,A = Tarski-Class X,(succ A)
assume A1: for A being Ordinal holds Tarski-Class X,A <> Tarski-Class X,(succ A) ; :: thesis: contradiction
defpred S₁[ set ] means ex A being Ordinal st $1 in Tarski-Class X,A;
consider Z being set such that
A2: for x being set holds
( x in Z iff ( x in Tarski-Class X & S₁[x] ) ) from XBOOLE_0:sch 1();
defpred S₂[ set , set ] means ex A being Ordinal st
( $2 = A & $1 in Tarski-Class X,(succ A) & not $1 in Tarski-Class X,A );
A3: for x, y, z being set st S₂[x,y] & S₂[x,z] holds
y = z

proof

let x, y, z be set ; :: thesis: ( S₂[x,y] & S₂[x,z] implies y = z )
given A being Ordinal such that A4: y = A and
A5: x in Tarski-Class X,(succ A) and
A6: not x in Tarski-Class X,A ; :: thesis: ( not S₂[x,z] or y = z )
given B being Ordinal such that A7: z = B and
A8: x in Tarski-Class X,(succ B) and
A9: not x in Tarski-Class X,B ; :: thesis: y = z
assume A10: y <> z ; :: thesis: contradiction
( A c= B or B c= A ) ;
then A12: ( A c< B or B c< A ) by A4, A7, A10, XBOOLE_0:def 8;

now

assume A c< B ; :: thesis: contradiction
then A in B by ORDINAL1:21;
then succ A c= B by ORDINAL1:33;
then Tarski-Class X,(succ A) c= Tarski-Class X,B by Th19;
hence contradiction by A5, A9; :: thesis: verum

end;

then B in A by A12, ORDINAL1:21;
then succ B c= A by ORDINAL1:33;
then Tarski-Class X,(succ B) c= Tarski-Class X,A by Th19;
hence contradiction by A6, A8; :: thesis: verum

end;

consider Y being set such that
A21: for x being set holds
( x in Y iff ex y being set st
( y in Z & S₂[y,x] ) ) from TARSKI:sch 1(A3);

now

let A be Ordinal; :: thesis: A in Y
A23: Tarski-Class X,A <> Tarski-Class X,(succ A) by A1;
A24: Tarski-Class X,A c= Tarski-Class X,(succ A) by Th18;
consider x being set such that
A25: ( ( x in Tarski-Class X,A & not x in Tarski-Class X,(succ A) ) or ( x in Tarski-Class X,(succ A) & not x in Tarski-Class X,A ) ) by A23, TARSKI:2;
x in Z by A2, A25;
hence A in Y by A21, A24, A25; :: thesis: verum

end;

hence contradiction by ORDINAL1:38; :: thesis: verum