Proposition is_maximal_is_strongly_maximal {X : dcpo} (CX : continuous_dcpo_struct X) {x : X} (Hx : is_strongly_maximal x) : is_maximal x. Proof. intros y p. use (invmap (continuous_dcpo_struct_le_via_approximation CX y x)). intros z q. assert (H := Hx z y q). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ r | r ]. - exact r. - apply fromempty. exact (is_hausdorff_separated_not_le (symm_is_hausdorff_separated r) p). 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.