const Union : set set const UPair : set set set term binunion = \x:set.\y:set.Union (UPair x y) const In : set set prop term iIn = In infix iIn 2000 2000 axiom UPairE: !x:set.!y:set.!z:set.x iIn UPair y z -> x = y | x = z axiom UnionE_impred: !x:set.!y:set.y iIn Union x -> !P:prop.(!z:set.y iIn z -> z iIn x -> P) -> P claim !x:set.!y:set.!z:set.z iIn binunion x y -> z iIn x | z iIn y