const SNoLev : set set const SNo_ : set set prop const ordinal : set prop const SNo : set prop const In : set set prop term iIn = In infix iIn 2000 2000 var x:set var y:set var P:prop var z:set hyp SNoLev y iIn x -> ordinal (SNoLev y) -> SNo y -> SNo_ (SNoLev y) y -> P hyp z iIn x hyp SNo y hyp ordinal (SNoLev y) hyp SNo_ (SNoLev y) y hyp SNoLev y = z claim SNoLev y iIn x -> P