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 SNo : set prop const ordinal : set prop axiom SNoLev_ordinal: !x:set.SNo x -> ordinal (SNoLev x) const SNo_ : set set prop lemma !x:set.SNo x -> ordinal (SNoLev x) -> SNo_ (ordsucc (SNoLev x)) (PSNo (ordsucc (SNoLev x)) \y:set.y iIn x & y != SNoLev x) claim !x:set.SNo x -> SNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)