const In : set set prop term iIn = In infix iIn 2000 2000 const Subq : set set prop term TransSet = \x:set.!y:set.y iIn x -> Subq y x term ordinal = \x:set.TransSet x & !y:set.y iIn x -> TransSet y const PNoLt_ : set (set prop) (set prop) prop const binintersect : set set set const PNoLt : set (set prop) set (set prop) prop axiom PNoLtI1: !x:set.!y:set.!p:set prop.!q:set prop.PNoLt_ (binintersect x y) p q -> PNoLt x p y q axiom or3I1: !P:prop.!Q:prop.!R:prop.P -> P | Q | R axiom binintersect_Subq_eq_1: !x:set.!y:set.Subq x y -> binintersect x y = x axiom Subq_ref: !x:set.Subq x x axiom binintersect_com: !x:set.!y:set.binintersect x y = binintersect y x axiom ordinal_trichotomy_or: !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | x = y | y iIn x axiom or3I3: !P:prop.!Q:prop.!R:prop.R -> P | Q | R const PNoEq_ : set (set prop) (set prop) prop axiom PNoLt_trichotomy_or_: !p:set prop.!q:set prop.!x:set.ordinal x -> PNoLt_ x p q | PNoEq_ x p q | PNoLt_ x q p lemma !x:set.!y:set.!p:set prop.!q:set prop.TransSet y -> PNoEq_ (binintersect x y) p q -> x iIn y -> binintersect x y = x -> PNoLt x p y q | x = y & PNoEq_ x p q | PNoLt y q x p lemma !x:set.!y:set.!p:set prop.!q:set prop.PNoEq_ (binintersect x y) p q -> x = y -> binintersect x y = x -> PNoLt x p y q | x = y & PNoEq_ x p q | PNoLt y q x p lemma !x:set.!y:set.!p:set prop.!q:set prop.TransSet x -> PNoEq_ (binintersect x y) p q -> y iIn x -> binintersect x y = y -> PNoLt x p y q | x = y & PNoEq_ x p q | PNoLt y q x p var x:set var y:set var p:set prop var q:set prop hyp ordinal x hyp ordinal y hyp TransSet x hyp TransSet y claim ordinal (binintersect x y) -> PNoLt x p y q | x = y & PNoEq_ x p q | PNoLt y q x p