const SNo : set prop const Empty : set axiom SNo_0: SNo Empty const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom SNoLe_tra: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x <= y -> y <= z -> x <= z const minus_SNo : set set term - = minus_SNo var x:set hyp SNo x hyp SNo - x hyp Empty <= x claim - x <= Empty -> - x <= x