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[ object ] means ex A being Ordinal st $1 in Tarski-Class (X,A);
consider Z being set such that
A2: for x being object holds
( x in Z iff ( x in Tarski-Class X & S1[x] ) ) from XBOOLE_0:sch 1();
 defpred S2[ object , object ] 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 object st S2[x,y] & S2[x,z] holds
y = z
proof
let x, y, z be object ; :: 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
( A c= B or B c= A ) ;
then A11: ( A c< B or B c< A ) by A4, A7, A10;
now :: thesis: not A c< B
assume A c< B ; :: thesis: contradiction
then succ A c= B by ORDINAL1:11, ORDINAL1:21;
then Tarski-Class (X,(succ A)) c= Tarski-Class (X,B) by Th16;
hence contradiction by A5, A9; :: thesis: verum
end;
then succ B c= A by ORDINAL1:11, ORDINAL1:21, A11;
then Tarski-Class (X,(succ B)) c= Tarski-Class (X,A) by Th16;
hence contradiction by A6, A8; :: thesis: verum
end;
consider Y being set such that
A12: for x being object holds
( x in Y iff ex y being object st
( y in Z & S2[y,x] ) ) from TARSKI:sch 1(A3);
now :: thesis: for A being Ordinal holds A in Y
let A be Ordinal; :: thesis: A in Y
A13: Tarski-Class (X,A) c= Tarski-Class (X,(succ A)) by Th15;
consider x being object such that
A14: ( ( 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 A1, TARSKI:2;
x in Z by A2, A14;
hence A in Y by A12, A13, A14; :: thesis: verum
end;
hence contradiction by ORDINAL1:26; :: thesis: verum