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