const SNo : set prop const Empty : set axiom SNo_0: SNo Empty const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom neg_mul_SNo_Lt: !x:set.!y:set.!z:set.SNo x -> x < Empty -> SNo y -> SNo z -> z < y -> x * y < x * z axiom mul_SNo_zeroR: !x:set.SNo x -> x * Empty = Empty const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom SNoLtLe: !x:set.!y:set.x < y -> x <= y axiom nonneg_mul_SNo_Le: !x:set.!y:set.!z:set.SNo x -> Empty <= x -> SNo y -> SNo z -> y <= z -> x * y <= x * z axiom SNoLtLe_or: !x:set.!y:set.SNo x -> SNo y -> x < y | y <= x claim !x:set.SNo x -> Empty <= x * x