theorem Th6: :: ZFMODEL1:6

for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_infinity iff 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 ) ) ) )