proposition: Lemma is_strongly_maximal_basis_2 {X : dcpo} (B : dcpo_basis X) (x : X) : is_strongly_maximal x → (∀ (i j : B), B i ≪ B j ⇒ (B i ≪ x ∨ is_hausdorff_separated (B j) x))%logic.
proof: Proof. intros HX i j p. exact (HX (B i) (B j) p). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Elements.Sharp