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 prop) prop axiom PNoLt_irref_: !x:set.!p:set prop.~ PNoLt_ x p p axiom In_irref: !x:set.nIn x x axiom FalseE: ~ False const PNoLt : set (set prop) set (set prop) prop const binintersect : set set set const PNoEq_ : set (set prop) (set prop) prop axiom PNoLtE: !x:set.!y:set.!p:set prop.!q:set prop.PNoLt x p y q -> !P:prop.(PNoLt_ (binintersect x y) p q -> P) -> (x iIn y -> PNoEq_ x p q -> q x -> P) -> (y iIn x -> PNoEq_ y p q -> ~ p y -> P) -> P claim !x:set.!p:set prop.~ PNoLt x p x p