const ordinal : set prop const SNo_ : set set prop const SNo : set prop axiom SNo_SNo: !x:set.ordinal x -> !y:set.SNo_ x y -> SNo y const minus_SNo : set set term - = minus_SNo lemma !x:set.!y:set.ordinal x -> SNo_ x y -> SNo y -> SNo_ x - y claim !x:set.ordinal x -> !y:set.SNo_ x y -> SNo_ x - y