Lemma is_strongly_maximal_basis_1 {X : dcpo} (B : dcpo_basis X) (x : X) : (∀ (i j : B), B i ≪ B j ⇒ (B i ≪ x ∨ is_hausdorff_separated (B j) x))%logic → is_strongly_maximal x. Proof. intros HB u v Huv. assert (Hb := basis_unary_interpolation B Huv). revert Hb. use factor_through_squash. { apply propproperty. } intros [i [Hui Hiv]]. assert (Hb := basis_unary_interpolation B Hiv). revert Hb. use factor_through_squash. { apply propproperty. } intros [j [Hij Hjv]]. specialize (HB _ _ Hij). revert HB. use factor_through_squash. { apply propproperty. } intros [Hix | Hsep]. { apply hinhpr. left. use (trans_way_below Hui Hix). } { apply hinhpr. right. use (is_hausdorff_separated_le _ _ _ _ Hsep). apply way_below_to_le, Hjv. } Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Elements.Sharp.