theorem Th2: :: ZFMODEL1:2

for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_pairs iff for u, v being Element of E holds {u,v} in E )