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