const CSNo : set prop const SNo : set prop const CSNo_Re : set set axiom CSNo_ReR: !x:set.CSNo x -> SNo (CSNo_Re x) const mul_CSNo : set set set lemma !x:set.!y:set.CSNo x -> CSNo y -> CSNo (mul_CSNo x y) -> CSNo (mul_CSNo y x) -> SNo (CSNo_Re x) -> mul_CSNo x y = mul_CSNo y x var x:set var y:set hyp CSNo x hyp CSNo y hyp CSNo (mul_CSNo x y) claim CSNo (mul_CSNo y x) -> mul_CSNo x y = mul_CSNo y x