const SNo : set prop const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const Empty : set const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom pos_mul_SNo_Lt: !x:set.!y:set.!z:set.SNo x -> Empty < x -> SNo y -> SNo z -> y < z -> x * y < x * z axiom mul_SNo_com: !x:set.!y:set.SNo x -> SNo y -> x * y = y * x claim !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> Empty < z -> x < y -> x * z < y * z