const SNo : set prop const ordsucc : set set const Empty : set axiom SNo_1: SNo (ordsucc Empty) const SNoLt : set set prop term < = SNoLt infix < 2020 2020 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 -> SNo y -> SNo z -> Empty < z -> x < y -> x * z < y * z axiom mul_SNo_oneL: !x:set.SNo x -> ordsucc Empty * x = x claim !x:set.!y:set.SNo x -> SNo y -> x < ordsucc Empty -> Empty < y -> x * y < y