const UPair : set set set term Sing = \x:set.UPair x x 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 claim !x:set.ZF_closed x -> !y:set.y iIn x -> Sing y iIn x