const ordinal : set prop const SNo_ : set set prop term SNo = \x:set.?y:set.ordinal y & SNo_ y x const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const PNoLt : set (set prop) set (set prop) prop const SNoLev : set set term SNoLt = \x:set.\y:set.PNoLt (SNoLev x) (\z:set.z iIn x) (SNoLev y) \z:set.z iIn y term < = SNoLt infix < 2020 2020 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 axiom PNoEq_sym_: !x:set.!p:set prop.!q:set prop.PNoEq_ x p q -> PNoEq_ x q p axiom PNoLtI3: !x:set.!y:set.!p:set prop.!q:set prop.y iIn x -> PNoEq_ y p q -> ~ p y -> PNoLt x p y q axiom PNoLtI2: !x:set.!y:set.!p:set prop.!q:set prop.x iIn y -> PNoEq_ x p q -> q x -> PNoLt x p y q const PSNo : set (set prop) set const binintersect : set set set var x:set var y:set var P:prop var z:set hyp !w:set.SNo w -> SNoLev w iIn binintersect (SNoLev x) (SNoLev y) -> SNoEq_ (SNoLev w) w x -> SNoEq_ (SNoLev w) w y -> x < w -> w < y -> nIn (SNoLev w) x -> SNoLev w iIn y -> P hyp z iIn binintersect (SNoLev x) (SNoLev y) hyp PNoEq_ z (\w:set.w iIn x) \w:set.w iIn y hyp ~ z iIn x hyp z iIn y hyp z iIn SNoLev x hyp z iIn SNoLev y hyp SNo (PSNo z \w:set.w iIn x) hyp SNoLev (PSNo z \w:set.w iIn x) = z hyp SNoEq_ z (PSNo z \w:set.w iIn x) x claim SNoEq_ z (PSNo z \w:set.w iIn x) y -> P