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_extend1 = \x:set.PSNo (ordsucc (SNoLev x)) \y:set.y iIn x | y = SNoLev x const PNoEq_ : set (set prop) (set prop) prop term SNoEq_ = \x:set.\y:set.\z:set.PNoEq_ x (\w:set.w iIn y) \w:set.w iIn z const SNo : set prop const ordinal : set prop axiom SNoLev_ordinal: !x:set.SNo x -> ordinal (SNoLev x) lemma !x:set.SNo x -> ordinal (SNoLev x) -> PNoEq_ (SNoLev x) (\y:set.y iIn PSNo (ordsucc (SNoLev x)) \z:set.z iIn x | z = SNoLev x) \y:set.y iIn x claim !x:set.SNo x -> SNoEq_ (SNoLev x) (SNo_extend1 x) x