const ordinal : set prop const ordsucc : set set const SNoLev : set set const SNo : set prop const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set var p:set prop var x:set hyp !y:set.ordinal y -> !z:set.z iIn SNoS_ y -> p z hyp SNo x hyp ordinal (ordsucc (SNoLev x)) claim x iIn SNoS_ (ordsucc (SNoLev x)) -> p x