proposition: Lemma next_or : forall a b c x y : E, is_ultra_linear_subset a b -> downward_saturated a b c -> is_bottom_element a (complement b c) x -> inc y b -> leq a y x -> x = y \/ inc y c.
proof: Proof. ir. assert (axioms a). uh H. ee. uh H; ee. uh H; ee. am. cp (leq_eq_or_lt H4 H3). nin H5. ap or_introl. sy; am. assert (x <> y -> inc y c). ir. apply use_complement with b. am. uf not; ir. uh H1; ee. uh H1; ee. cp (H11 y H7). assert (x = y). apply leq_leq_eq with a. am. am. am. ap H6; am. ap excluded_middle. uf not; ir. ap H7. ap or_introl. ap excluded_middle. uf not; ir. ap H7. ap or_intror. ap H6; am. Qed.
imports: universe