const CSNo : set prop const Complex_i : set axiom CSNo_Complex_i: CSNo Complex_i const mul_CSNo : set set set axiom CSNo_mul_CSNo: !x:set.!y:set.CSNo x -> CSNo y -> CSNo (mul_CSNo x y) const minus_CSNo : set set const ordsucc : set set const Empty : set lemma CSNo (mul_CSNo Complex_i Complex_i) -> mul_CSNo Complex_i Complex_i = minus_CSNo (ordsucc Empty) claim mul_CSNo Complex_i Complex_i = minus_CSNo (ordsucc Empty)