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 )
assume A1: x c< A ; :: thesis: x in A
then A2: x c= A by XBOOLE_0:def 8;
consider a being Element of A \ x;
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: ( y in A & not y in x ) by A3, XBOOLE_0:def 5;
A6: y c= A by A3, Def2;

now

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

end;

then A8: y c= x by TARSKI:def 3;

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
A9: ( z = a & z in x ) ;
z c= x by A9, Def2;
then not y in z by A3, XBOOLE_0:def 5;
hence a in y by A2, A5, A9, Def3; :: thesis: verum

end;

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