let x be epsilon-transitive set ; for A being Ordinal st x c< A holds
x in A
let A be Ordinal; ( x c< A implies x in A )
set a = the Element of A \ x;
assume A1:
x c< A
; 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;
then A8:
x c= y
;
A9:
y c= A
by A3, Def2;
then A11:
y c= x
;
y in A
by A3;
hence
x in A
by A11, A8, XBOOLE_0:def 10; verum