const PNoLt_ : set (set prop) (set prop) prop const binintersect : set set set const In : set set prop term iIn = In infix iIn 2000 2000 const PNoEq_ : set (set prop) (set prop) prop term PNoLt = \x:set.\p:set prop.\y:set.\q:set prop.PNoLt_ (binintersect x y) p q | x iIn y & PNoEq_ x p q & q x | y iIn x & PNoEq_ y p q & ~ p y axiom or3I3: !P:prop.!Q:prop.!R:prop.R -> P | Q | R claim !x:set.!y:set.!p:set prop.!q:set prop.y iIn x -> PNoEq_ y p q -> ~ p y -> PNoLt x p y q