let E be non empty set ; :: thesis:
assume A1: E is epsilon-transitive ; :: thesis:
thus ( E |= the_axiom_of_infinity implies ex X being set st
( X in E & X <> {} & ( for Y being set st Y in X holds
ex Z being set st
( Y c< Z & Z in X ) ) ) ) :: thesis:

proof

assume E |= the_axiom_of_infinity ; :: thesis:
then consider u being Element of E such that
A2: u <> {} and
A3: for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) by A1, Th6;
reconsider X = u as set ;
take X ; :: thesis:
thus ( X in E & X <> {} ) by A2; :: thesis:
let Y be set ; :: thesis:
assume A4: Y in X ; :: thesis:
X c= E by A1;
then reconsider v = Y as Element of E by A4;
consider w being Element of E such that
A5: ( v c< w & w in u ) by A3, A4;
reconsider w = w as set ;
take w ; :: thesis:
thus ( Y c< w & w in X ) by A5; :: thesis:

end;

given X being set such that A6: X in E and
A7: X <> {} and
A8: for Y being set st Y in X holds
ex Z being set st
( Y c< Z & Z in X ) ; :: thesis:
ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) )

proof

reconsider u = X as Element of E by A6;
take u ; :: thesis:
thus u <> {} by A7; :: thesis:
let v be Element of E; :: thesis:
assume v in u ; :: thesis:
then consider Z being set such that
A9: v c< Z and
A10: Z in X by A8;
X c= E by A1, A6;
then reconsider w = Z as Element of E by A10;
take w ; :: thesis:
thus ( v c< w & w in u ) by A9, A10; :: thesis:

end;

hence E |= the_axiom_of_infinity by A1, Th6; :: thesis: