const PSNo : set (set prop) set const ordsucc : set set const SNoLev : set set const In : set set prop term iIn = In infix iIn 2000 2000 term SNo_extend0 = \x:set.PSNo (ordsucc (SNoLev x)) \y:set.y iIn x & y != SNoLev x const ordinal : set prop axiom ordinal_ordsucc: !x:set.ordinal x -> ordinal (ordsucc x) const SNo_ : set set prop axiom SNo_PSNo: !x:set.ordinal x -> !p:set prop.SNo_ x (PSNo x p) const SNo : set prop var x:set hyp SNo x claim ordinal (SNoLev x) -> SNo_ (ordsucc (SNoLev x)) (PSNo (ordsucc (SNoLev x)) \y:set.y iIn x & y != SNoLev x)