const In : set set prop term iIn = In infix iIn 2000 2000 const real : set const SNo : set prop axiom real_SNo: !x:set.x iIn real -> SNo x const CSNo : set prop const SNo_pair : set set set axiom CSNo_I: !x:set.!y:set.SNo x -> SNo y -> CSNo (SNo_pair x y) const complex : set axiom complex_E: !x:set.x iIn complex -> !P:prop.(!y:set.y iIn real -> !z:set.z iIn real -> x = SNo_pair y z -> P) -> P claim !x:set.x iIn complex -> CSNo x