const SNo : set prop const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom SNo_mul_SNo: !x:set.!y:set.SNo x -> SNo y -> SNo (x * y) const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const Empty : set 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 SNo_0: SNo Empty axiom SNoLt_tra: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x < y -> y < z -> x < z axiom pos_mul_SNo_Lt': !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> Empty < z -> x < y -> x * z < y * z claim !x:set.!y:set.!z:set.!w:set.SNo x -> SNo y -> SNo z -> SNo w -> Empty < x -> Empty < y -> x < z -> y < w -> x * y < z * w