const SNo : set prop const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom add_SNo_Lt1: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x < z -> (x + y) < z + y axiom add_SNo_com: !x:set.!y:set.SNo x -> SNo y -> x + y = y + x const minus_SNo : set set term - = minus_SNo const Empty : set var x:set var y:set var z:set hyp SNo x hyp SNo - x hyp y = z + x hyp SNo z hyp - x < z hyp SNo - z hyp - z + z = Empty claim - z < x -> Empty < y