const Union : set set const UPair : set set set term binunion = \x:set.\y:set.Union (UPair x y) const ZF_closed : set prop const In : set set prop term iIn = In infix iIn 2000 2000 axiom ZF_UPair_closed: !x:set.ZF_closed x -> !y:set.y iIn x -> !z:set.z iIn x -> UPair y z iIn x axiom ZF_Union_closed: !x:set.ZF_closed x -> !y:set.y iIn x -> Union y iIn x claim !x:set.ZF_closed x -> !y:set.y iIn x -> !z:set.z iIn x -> binunion y z iIn x