const In : set set prop term iIn = In infix iIn 2000 2000 const Union : set set axiom UnionEq: !x:set.!y:set.y iIn Union x <-> ?z:set.y iIn z & z iIn x claim !x:set.!y:set.!z:set.y iIn z -> z iIn x -> y iIn Union x