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₁[ set ] means ex A being Ordinal st $1 in Rank A;
consider Power being set such that
A3: for x being set holds
( x in Power iff ( x in Tarski-Class X & S₁[x] ) ) from XBOOLE_0:sch 1();
defpred S₂[ set , set ] means ex A being Ordinal st
( $2 = A & not $1 in Rank A & $1 in Rank (succ A) );
A4: for x, y, z being set st S₂[x,y] & S₂[x,z] holds
y = z

proof

let x, y, z be set ; :: 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 ( A1 in A2 or A2 in A1 ) by A5, A8, ORDINAL1:24;
then A13: ( succ A1 c= A2 or succ A2 c= A1 ) by ORDINAL1:33;

now

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

end;

then Rank (succ A2) c= Rank A1 by A13, Th43;
hence contradiction by A6, A10; :: thesis: verum

end;

consider Y being set such that
A18: for x being set holds
( x in Y iff ex y being set st
( y in Power & S₂[y,x] ) ) from TARSKI:sch 1(A4);

now

let A be Ordinal; :: thesis: A in Y
(Rank A) /\ (Tarski-Class X) <> (Rank (succ A)) /\ (Tarski-Class X) by A1, A2, Th52;
then consider y being set such that
A21: ( ( 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;
A in succ A by ORDINAL1:10;
then A c= succ A by ORDINAL1:def 2;
then A24: Rank A c= Rank (succ A) by Th43;
then (Rank A) /\ (Tarski-Class X) c= (Rank (succ A)) /\ (Tarski-Class X) by XBOOLE_1:26;
then A26: y in Rank (succ A) by A21, XBOOLE_0:def 4;
A27: y in Tarski-Class X by A21, XBOOLE_0:def 4;
A28: ( not y in Rank A or not y in Tarski-Class X ) by A21, A24, XBOOLE_0:def 4;
y in Power by A3, A26, A27;
hence A in Y by A18, A21, A26, A28, XBOOLE_0:def 4; :: thesis: verum

end;

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