const SNo : set prop const ordinal : set prop const SNoLev : set set axiom SNoLev_ordinal: !x:set.SNo x -> ordinal (SNoLev x) const Subq : set set prop const minus_SNo : set set term - = minus_SNo lemma !x:set.SNo x -> ordinal (SNoLev x) -> Subq (SNoLev - x) (SNoLev x) claim !x:set.SNo x -> Subq (SNoLev - x) (SNoLev x)