const minus_SNo : set set term - = minus_SNo const Empty : set axiom minus_SNo_0: - Empty = Empty const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 const SNo : set prop const abs_SNo : set set var x:set hyp SNo x hyp Empty <= x hyp Empty <= - x claim x = Empty -> abs_SNo - x = abs_SNo x