let W be Universe; :: thesis: W |= the_axiom_of_pairs
( W is epsilon-transitive & ( for u, v being Element of W holds {u,v} in W ) ) ;
hence W |= the_axiom_of_pairs by ZFMODEL1:2; :: thesis: verum