const bij : set set (set set) prop term equip = \x:set.\y:set.?f:set set.bij x y f const In : set set prop term iIn = In infix iIn 2000 2000 term PNoEq_ = \x:set.\p:set prop.\q:set prop.!y:set.y iIn x -> (p y <-> q y) term nIn = \x:set.\y:set.~ x iIn y 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 SNoLev : set set const binintersect : set set set const SNoElts_ : set set axiom restr_SNoLev: !x:set.SNo x -> !y:set.y iIn SNoLev x -> SNoLev (binintersect x (SNoElts_ y)) = y const nat_p : set prop const ordsucc : set set const Sep : set (set prop) set const SNoS_ : set set const omega : set lemma !x:set.!y:set.!P:prop.nat_p x -> SNoLev y = ordsucc x -> SNo y -> (SNo y -> SNoLev y = ordsucc x -> binintersect y (SNoElts_ x) iIn Sep (SNoS_ omega) (\z:set.SNoLev z = x) -> SNo (binintersect y (SNoElts_ x)) -> SNoLev (binintersect y (SNoElts_ x)) = x -> P) -> x iIn SNoLev y -> SNoLev (binintersect y (SNoElts_ x)) = x -> P var x:set var y:set var P:prop hyp nat_p x hyp SNoLev y = ordsucc x hyp SNo y hyp SNo y -> SNoLev y = ordsucc x -> binintersect y (SNoElts_ x) iIn Sep (SNoS_ omega) (\z:set.SNoLev z = x) -> SNo (binintersect y (SNoElts_ x)) -> SNoLev (binintersect y (SNoElts_ x)) = x -> P claim x iIn SNoLev y -> P