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 S1[ 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 & S1[x] ) ) from XBOOLE_0:sch 1();
 defpred S2[ 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 S2[x,y] & S2[x,z] holds
y = z
proof
let x, y, z be set ; :: thesis: ( S2[x,y] & S2[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 S2[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 A11: y <> z ; :: thesis: contradiction
A12: ( A1 in A2 or A2 in A1 ) by A5, A8, A11, ORDINAL1:24;
A13: ( succ A1 c= A2 or succ A2 c= A1 ) by A12, ORDINAL1:33;
A14: now
assume A15: succ A1 c= A2 ; :: thesis: contradiction
A16: Rank (succ A1) c= Rank A2 by A15, Th43;
thus contradiction by A7, A9, A16; :: thesis: verum
end;
A17: Rank (succ A2) c= Rank A1 by A13, A14, Th43;
thus contradiction by A6, A10, A17; :: 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 & S2[y,x] ) ) from TARSKI:sch 1(A4);
A19: now
let A be Ordinal; :: thesis: A in Y
A20: (Rank A) /\ (Tarski-Class X) <> (Rank (succ A)) /\ (Tarski-Class X) by A1, A2, Th52;
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 A20, TARSKI:2;
A22: A in succ A by ORDINAL1:10;
A23: A c= succ A by A22, ORDINAL1:def 2;
A24: Rank A c= Rank (succ A) by A23, Th43;
A25: (Rank A) /\ (Tarski-Class X) c= (Rank (succ A)) /\ (Tarski-Class X) by A24, XBOOLE_1:26;
A26: y in Rank (succ A) by A21, A25, 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;
A29: y in Power by A3, A26, A27;
thus A in Y by A18, A21, A26, A28, A29, XBOOLE_0:def 4; :: thesis: verum
end;
thus contradiction by A19, ORDINAL1:38; :: thesis: verum