const PNoEq_ : set (set prop) (set prop) prop const In : set set prop term iIn = In infix iIn 2000 2000 term SNoEq_ = \x:set.\y:set.\z:set.PNoEq_ x (\w:set.w iIn y) \w:set.w iIn z axiom PNoEq_sym_: !x:set.!p:set prop.!q:set prop.PNoEq_ x p q -> PNoEq_ x q p claim !x:set.!y:set.!z:set.SNoEq_ x y z -> SNoEq_ x z y