theorem :: ZFMODEL1:7

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