let X be set ; :: thesis: ( X is epsilon-transitive implies ex A being Ordinal st Tarski-Class X c= Rank A )
assume A1: X is epsilon-transitive ; :: thesis: ex A being Ordinal st Tarski-Class X c= Rank A
assume A2: for A being Ordinal holds not Tarski-Class X c= Rank A ; :: thesis: contradiction
defpred S₁[ object ] means ex A being Ordinal st $1 in Rank A;
consider Power being set such that
A3: for x being object holds
( x in Power iff ( x in Tarski-Class X & S₁[x] ) ) from XBOOLE_0:sch 1();
defpred S₂[ object , object ] means ex A being Ordinal st
( $2 = A & not $1 in Rank A & $1 in Rank (succ A) );
A4: for x, y, z being object st S₂[x,y] & S₂[x,z] holds
y = z

proof

let x, y, z be object ; :: thesis: ( S₂[x,y] & S₂[x,z] implies y = z )
given A1 being Ordinal such that A5: y = A1 and
A6: not x in Rank A1 and
A7: x in Rank (succ A1) ; :: thesis: ( not S₂[x,z] or y = z )
given A2 being Ordinal such that A8: z = A2 and
A9: not x in Rank A2 and
A10: x in Rank (succ A2) ; :: thesis: y = z
assume y <> z ; :: thesis: contradiction
then A11: ( A1 in A2 or A2 in A1 ) by A5, A8, ORDINAL1:14;

now :: thesis: not succ A1 c= A2

assume succ A1 c= A2 ; :: thesis: contradiction
then Rank (succ A1) c= Rank A2 by Th37;
hence contradiction by A7, A9; :: thesis: verum

end;

then Rank (succ A2) c= Rank A1 by A11, Th37, ORDINAL1:21;
hence contradiction by A6, A10; :: 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 Power & S₂[y,x] ) ) from TARSKI:sch 1(A4);

now :: thesis: for A being Ordinal holds A in Y

let A be Ordinal; :: thesis: A in Y
(Rank A) /\ (Tarski-Class X) <> (Rank (succ A)) /\ (Tarski-Class X) by A1, A2, Th46;
then consider y being object such that
A13: ( ( y in (Rank A) /\ (Tarski-Class X) & not y in (Rank (succ A)) /\ (Tarski-Class X) ) or ( y in (Rank (succ A)) /\ (Tarski-Class X) & not y in (Rank A) /\ (Tarski-Class X) ) ) by TARSKI:2;
A14: A c= succ A by ORDINAL1:6, ORDINAL1:def 2;
then A15: Rank A c= Rank (succ A) by Th37;
(Rank A) /\ (Tarski-Class X) c= (Rank (succ A)) /\ (Tarski-Class X) by XBOOLE_1:26, A14, Th37;
then A16: y in Rank (succ A) by A13, XBOOLE_0:def 4;
A17: y in Tarski-Class X by A13, XBOOLE_0:def 4;
then A18: not y in Rank A by A13, A15, XBOOLE_0:def 4;
y in Power by A3, A16, A17;
hence A in Y by A12, A16, A18; :: thesis: verum

end;

hence contradiction by ORDINAL1:26; :: thesis: verum