const SNo : set prop const minus_SNo : set set term - = minus_SNo axiom SNo_minus_SNo: !x:set.SNo x -> SNo - x const SNo_ : set set prop const SNoLev : set set axiom SNoLev_: !x:set.SNo x -> SNo_ (SNoLev x) x var x:set var y:set hyp SNo y hyp SNoLev y = x claim SNoLev - y = x -> SNo_ x - y