let A be Ordinal; :: thesis:
let X be set ; :: thesis:
assume that
A1: X is epsilon-transitive and
A2: A in the_rank_of X ; :: thesis:
defpred S₂[ Ordinal] means ex Y being set st
( A in $1 & Y in X & the_rank_of Y = $1 );
assume A3: for Y being set holds
( not Y in X or not the_rank_of Y = A ) ; :: thesis:
A4: ex B being Ordinal st S₂[B]

assume A5: for B being Ordinal
for Y being set st A in B & Y in X holds
the_rank_of Y <> B ; :: thesis:
X c= Rank A

let x be object ; :: according to TARSKI:def 3 :: thesis:
reconsider xx = x as set by TARSKI:1;
assume A6: x in X ; :: thesis:
then A7: the_rank_of xx <> A by A3;
the_rank_of xx c= A by A5, A6, ORDINAL1:16;
then the_rank_of xx c< A by A7;
then the_rank_of xx in A by ORDINAL1:11;
hence x in Rank A by CLASSES1:66; :: thesis:

end;

then the_rank_of X c= A by CLASSES1:65;
hence contradiction by A2, ORDINAL1:5; :: thesis:

end;

consider B being Ordinal such that
A8: S₂[B] and
A9: for C being Ordinal st S₂[C] holds
B c= C from ORDINAL1:sch 1(A4);
consider Y being set such that
A10: A in B and
A11: Y in X and
A12: the_rank_of Y = B by A8;
Y c= Rank A

let x be object ; :: according to TARSKI:def 3 :: thesis:
reconsider xx = x as set by TARSKI:1;
A13: Y c= X by A1, A11;
assume A14: x in Y ; :: thesis:
then the_rank_of xx in B by A12, CLASSES1:68;
then not A in the_rank_of xx by A9, A14, A13, ORDINAL1:5;
then A15: the_rank_of xx c= A by ORDINAL1:16;
the_rank_of xx <> A by A3, A14, A13;
then the_rank_of xx c< A by A15;
then the_rank_of xx in A by ORDINAL1:11;
hence x in Rank A by CLASSES1:66; :: thesis:

end;

then the_rank_of Y c= A by CLASSES1:65;
hence contradiction by A10, A12, ORDINAL1:5; :: thesis: