let x be epsilon-transitive set ; :: thesis: for A being Ordinal st x c< A holds
x in A
let A be Ordinal; :: thesis: ( x c< A implies x in A )
consider a being Element of A \ x;
assume A1: x c< A ; :: thesis: x in A
then A2: x c= A by XBOOLE_0:def 8;
A \ x <> {}

proof

assume A \ x = {} ; :: thesis: contradiction
then A c= x by XBOOLE_1:37;
hence contradiction by A1, XBOOLE_1:60; :: thesis: verum

end;

then a in A \ x ;
then consider y being set such that
A3: y in A \ x and
A4: for a being set holds
( not a in A \ x or not a in y ) by TARSKI:7;
A5: not y in x by A3, XBOOLE_0:def 5;

now

let a be set ; :: thesis: ( a in x implies a in y )
assume a in x ; :: thesis: a in y
then consider z being set such that
A6: z = a and
A7: z in x ;
z c= x by A7, Def2;
then not y in z by A3, XBOOLE_0:def 5;
hence a in y by A2, A3, A5, A6, A7, Def3; :: thesis: verum

end;

then A8: x c= y by TARSKI:def 3;
A9: y c= A by A3, Def2;

now

let a be set ; :: thesis: ( a in y implies a in x )
assume A10: a in y ; :: thesis: a in x
then not a in A \ x by A4;
hence a in x by A9, A10, XBOOLE_0:def 5; :: thesis: verum

end;

then A11: y c= x by TARSKI:def 3;
y in A by A3;
hence x in A by A11, A8, XBOOLE_0:def 10; :: thesis: verum