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:

assume E |= the_axiom_of_infinity ; :: thesis:
then consider u being Element of E such that
A2: ( 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 ) ) ) 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 A3: Y in X ; :: thesis:
X c= E by A1, ORDINAL1:def 2;
then reconsider v = Y as Element of E by A3;
consider w being Element of E such that
A4: ( v c< w & w in u ) by A2, A3;
reconsider w = w as set ;
take w ; :: thesis:
thus ( Y c< w & w in X ) by A4; :: thesis:

end;

given X being set such that A5: ( 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:
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 ) ) )

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

end;

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