const SNo_pair : set set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 const CSNo_Re : set set const CSNo_Im : set set term add_CSNo = \x:set.\y:set.SNo_pair (CSNo_Re x + CSNo_Re y) (CSNo_Im x + CSNo_Im y) const In : set set prop term iIn = In infix iIn 2000 2000 const complex : set const real : set axiom complex_Re_real: !x:set.x iIn complex -> CSNo_Re x iIn real axiom real_add_SNo: !x:set.x iIn real -> !y:set.y iIn real -> x + y iIn real axiom complex_Im_real: !x:set.x iIn complex -> CSNo_Im x iIn real axiom complex_I: !x:set.x iIn real -> !y:set.y iIn real -> SNo_pair x y iIn complex claim !x:set.x iIn complex -> !y:set.y iIn complex -> add_CSNo x y iIn complex