const ordinal : set prop const SNo_ : set set prop const SNoLev : set set axiom SNoLev_uniq2: !x:set.ordinal x -> !y:set.SNo_ x y -> SNoLev y = x const SNo : set prop const minus_SNo : set set term - = minus_SNo lemma !x:set.!y:set.ordinal x -> SNo_ x y -> SNo y -> SNoLev y = x -> SNo_ x - y var x:set var y:set hyp ordinal x hyp SNo_ x y claim SNo y -> SNo_ x - y