theorem Th4: :: ZFMODEL1:4

for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_unions iff for u being Element of E holds union u in E )