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 S1[ 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 & S1[x] ) ) from XBOOLE_0:sch 1();
 defpred S2[ 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 S2[x,y] & S2[x,z] holds
y = z
proof
let x, y, z be set ; :: thesis: ( S2[x,y] & S2[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 S2[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
A11: ( A c= B or B c= A ) ;
A12: ( A c< B or B c< A ) by A4, A7, A10, A11, XBOOLE_0:def 8;
A13: now
assume A14: A c< B ; :: thesis: contradiction
A15: A in B by A14, ORDINAL1:21;
A16: succ A c= B by A15, ORDINAL1:33;
A17: Tarski-Class X,(succ A) c= Tarski-Class X,B by A16, Th19;
thus contradiction by A5, A9, A17; :: thesis: verum
end;
A18: B in A by A12, A13, ORDINAL1:21;
A19: succ B c= A by A18, ORDINAL1:33;
A20: Tarski-Class X,(succ B) c= Tarski-Class X,A by A19, Th19;
thus contradiction by A6, A8, A20; :: 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 & S2[y,x] ) ) from TARSKI:sch 1(A3);
A22: 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;
A26: x in Z by A2, A25;
thus A in Y by A21, A24, A25, A26; :: thesis: verum
end;
thus contradiction by A22, ORDINAL1:38; :: thesis: verum