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

proof

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Rank A )
assume A5: x in X ; :: thesis: x in Rank A
then not A in the_rank_of x by A4;
then ( the_rank_of x c= A & the_rank_of x <> A ) by A2, A5, ORDINAL1:26;
then the_rank_of x c< A by XBOOLE_0:def 8;
then the_rank_of x in A by ORDINAL1:21;
hence x in Rank A by CLASSES1:74; :: thesis: verum

end;

then the_rank_of X c= A by CLASSES1:73;
hence contradiction by A1, ORDINAL1:7; :: thesis: verum

end;

consider B being Ordinal such that
A6: S₂[B] and
A7: for C being Ordinal st S₂[C] holds
B c= C from ORDINAL1:sch 1(A3);
consider Y being set such that
A8: ( A in B & Y in X & the_rank_of Y = B ) by A6;
Y c= Rank A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in Rank A )
assume A9: x in Y ; :: thesis: x in Rank A
then A10: ( the_rank_of x in B & Y c= X ) by A1, A8, CLASSES1:76, ORDINAL1:def 2;
then not A in the_rank_of x by A7, A9, ORDINAL1:7;
then ( the_rank_of x c= A & the_rank_of x <> A ) by A2, A9, A10, ORDINAL1:26;
then the_rank_of x c< A by XBOOLE_0:def 8;
then the_rank_of x in A by ORDINAL1:21;
hence x in Rank A by CLASSES1:74; :: thesis: verum

end;

then the_rank_of Y c= A by CLASSES1:73;
hence contradiction by A8, ORDINAL1:7; :: thesis: verum