const SNo_pair : set set set const minus_SNo : set set term - = minus_SNo const CSNo_Re : set set const CSNo_Im : set set term minus_CSNo = \x:set.SNo_pair (- CSNo_Re x) - CSNo_Im x const CSNo : set prop const SNo : set prop axiom CSNo_ReR: !x:set.CSNo x -> SNo (CSNo_Re x) axiom SNo_minus_SNo: !x:set.SNo x -> SNo - x axiom CSNo_ImR: !x:set.CSNo x -> SNo (CSNo_Im x) axiom CSNo_Re2: !x:set.!y:set.SNo x -> SNo y -> CSNo_Re (SNo_pair x y) = x claim !x:set.CSNo x -> CSNo_Re (minus_CSNo x) = - CSNo_Re x