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 ordinal : set prop axiom ordinal_ordsucc: !x:set.ordinal x -> ordinal (ordsucc x) axiom ordsuccI2: !x:set.x iIn ordsucc x axiom PNoEq_PSNo: !x:set.ordinal x -> !p:set prop.PNoEq_ x (\y:set.y iIn PSNo x p) p axiom PNoEq_antimon_: !p:set prop.!q:set prop.!x:set.ordinal x -> !y:set.y iIn x -> PNoEq_ x p q -> PNoEq_ y p q axiom PNo_extend1_eq: !x:set.!p:set prop.PNoEq_ x p \y:set.p y | y = x axiom PNoEq_sym_: !x:set.!p:set prop.!q:set prop.PNoEq_ x p q -> PNoEq_ x q p axiom PNoEq_tra_: !x:set.!p:set prop.!q:set prop.!p2:set prop.PNoEq_ x p q -> PNoEq_ x q p2 -> PNoEq_ x p p2 const SNo : set prop var x:set hyp SNo x claim 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