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 )
set a = the Element of A \ x;
assume A1: x c< A ; :: thesis: x in A
then A2: x c= A ;
A \ x <> {} by A1, XBOOLE_1:37, XBOOLE_1:60;
then the Element of A \ x in A \ x ;
then consider y being set such that
A3: y in A \ x and
A4: for a being object holds
( not a in A \ x or not a in y ) by TARSKI:3;
A5: not y in x by A3, XBOOLE_0:def 5;

now :: thesis: for a being object st a in x holds
a in y

let a be object ; :: 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 ;
A9: y c= A by A3, Def2;

now :: thesis: for a being object st a in y holds
a in x

let a be object ; :: 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 ;
y in A by A3;
hence x in A by A11, A8, XBOOLE_0:def 10; :: thesis: verum