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 that
A1: X is epsilon-transitive and
A2: A in the_rank_of X ; :: thesis: ex Y being set st
( Y in X & the_rank_of Y = A )
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: contradiction
A4: ex B being Ordinal st S₂[B]

proof

assume A5: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Rank A )
reconsider xx = x as set by TARSKI:1;
assume A6: x in X ; :: thesis: x in Rank A
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: verum

end;

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

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in Rank A )
reconsider xx = x as set by TARSKI:1;
A13: Y c= X by A1, A11;
assume A14: x in Y ; :: thesis: x in Rank A
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: verum

end;

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