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 axiom iffEL: !P:prop.!Q:prop.(P <-> Q) -> P -> Q claim !x:set.!y:set.y iIn Union x -> ?z:set.y iIn z & z iIn x