const In : set set prop term iIn = In infix iIn 2000 2000 const Union : set set axiom UnionE: !x:set.!y:set.y iIn Union x -> ?z:set.y iIn z & z iIn x claim !x:set.!y:set.y iIn Union x -> !P:prop.(!z:set.y iIn z -> z iIn x -> P) -> P