let W be Universe; :: thesis: W |= the_axiom_of_unions
( W is epsilon-transitive & ( for u being Element of W holds union u in W ) ) ;
hence W |= the_axiom_of_unions by ZFMODEL1:4; :: thesis: verum