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