theorem Th1: :: ZF_REFLE:1
for W being Universe holds W |= the_axiom_of_pairs