const SNo : set prop const Empty : set axiom SNo_0: SNo Empty const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom SNoLtLe_tra: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x < y -> y <= z -> x < z axiom SNoLt_irref: !x:set.~ x < x const abs_SNo : set set const minus_SNo : set set term - = minus_SNo axiom not_nonneg_abs_SNo: !x:set.~ Empty <= x -> abs_SNo x = - x claim !x:set.SNo x -> x < Empty -> abs_SNo x = - x