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 PNoLt_ = \x:set.\p:set prop.\q:set prop.?y:set.y iIn x & (PNoEq_ y p q & ~ p y & q y) const ordinal : set prop axiom PNoEq_antimon_: !p:set prop.!q:set prop.!x:set.ordinal x -> !y:set.y iIn x -> PNoEq_ x p q -> PNoEq_ y p q axiom PNoEq_tra_: !x:set.!p:set prop.!q:set prop.!p2:set prop.PNoEq_ x p q -> PNoEq_ x q p2 -> PNoEq_ x p p2 axiom ordinal_trichotomy_or: !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | x = y | y iIn x var x:set var p:set prop var q:set prop var p2:set prop var y:set var z:set hyp ordinal x hyp y iIn x hyp PNoEq_ y p q hyp ~ p y hyp q y hyp z iIn x hyp PNoEq_ z q p2 hyp ~ q z hyp p2 z hyp ordinal y claim ordinal z -> ?w:set.w iIn x & (PNoEq_ w p p2 & ~ p w & p2 w)