proposition: 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: 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.
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