const ordinal : set prop const In : set set prop term iIn = In infix iIn 2000 2000 const SNo_ : set set prop const SNoS_ : set set axiom SNoS_I: !x:set.ordinal x -> !y:set.!z:set.z iIn x -> SNo_ z y -> y iIn SNoS_ x const SNoLev : set set const minus_SNo : set set term - = minus_SNo var x:set var y:set hyp ordinal x hyp SNoLev y iIn x hyp ordinal (SNoLev y) hyp SNo_ (SNoLev y) y claim SNo_ (SNoLev y) - y -> - y iIn SNoS_ x