let E be non empty set ; :: thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_infinity iff 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 ) ) ) ) )

assume A1: E is epsilon-transitive ; :: thesis: ( E |= the_axiom_of_infinity iff 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 ) ) ) )

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: ( 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 ) ) ) implies E |= the_axiom_of_infinity )

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: E |= the_axiom_of_infinity

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 ) ) )

( X in E & X <> {} & ( for Y being set st Y in X holds

ex Z being set st

( Y c< Z & Z in X ) ) ) ) )

assume A1: E is epsilon-transitive ; :: thesis: ( E |= the_axiom_of_infinity iff 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 ) ) ) )

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: ( 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 ) ) ) implies E |= the_axiom_of_infinity )

proof

given X being set such that A6:
X in E
and
assume
E |= the_axiom_of_infinity
; :: thesis: 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 ) ) )

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: ( X in E & X <> {} & ( for Y being set st Y in X holds

ex Z being set st

( Y c< Z & Z in X ) ) )

thus ( X in E & X <> {} ) by A2; :: thesis: for Y being set st Y in X holds

ex Z being set st

( Y c< Z & Z in X )

let Y be set ; :: thesis: ( Y in X implies ex Z being set st

( Y c< Z & Z in X ) )

assume A4: Y in X ; :: thesis: ex Z being set st

( Y c< Z & Z in X )

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: ( Y c< w & w in X )

thus ( Y c< w & w in X ) by A5; :: thesis: verum

end;( X in E & X <> {} & ( for Y being set st Y in X holds

ex Z being set st

( Y c< Z & Z in X ) ) )

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: ( X in E & X <> {} & ( for Y being set st Y in X holds

ex Z being set st

( Y c< Z & Z in X ) ) )

thus ( X in E & X <> {} ) by A2; :: thesis: for Y being set st Y in X holds

ex Z being set st

( Y c< Z & Z in X )

let Y be set ; :: thesis: ( Y in X implies ex Z being set st

( Y c< Z & Z in X ) )

assume A4: Y in X ; :: thesis: ex Z being set st

( Y c< Z & Z in X )

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: ( Y c< w & w in X )

thus ( Y c< w & w in X ) by A5; :: thesis: verum

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: E |= the_axiom_of_infinity

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

hence
E |= the_axiom_of_infinity
by A1, Th6; :: thesis: verum
reconsider u = X as Element of E by A6;

take u ; :: thesis: ( 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 ) ) )

thus u <> {} by A7; :: thesis: for v being Element of E st v in u holds

ex w being Element of E st

( v c< w & w in u )

let v be Element of E; :: thesis: ( v in u implies ex w being Element of E st

( v c< w & w in u ) )

assume v in u ; :: thesis: ex w being Element of E st

( v c< w & w in u )

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: ( v c< w & w in u )

thus ( v c< w & w in u ) by A9, A10; :: thesis: verum

end;take u ; :: thesis: ( 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 ) ) )

thus u <> {} by A7; :: thesis: for v being Element of E st v in u holds

ex w being Element of E st

( v c< w & w in u )

let v be Element of E; :: thesis: ( v in u implies ex w being Element of E st

( v c< w & w in u ) )

assume v in u ; :: thesis: ex w being Element of E st

( v c< w & w in u )

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: ( v c< w & w in u )

thus ( v c< w & w in u ) by A9, A10; :: thesis: verum