Lemma is_hausdorff_separated_le (x y z : X) : y ⊑ z → is_hausdorff_separated y x → is_hausdorff_separated z x. Proof. intros Hyz. use factor_through_squash_hProp. intros (S1 & S2 & H1 & H2 & Hdisj). apply hinhpr. use (S1,, S2,, _,, H2,, Hdisj). exact (is_scott_open_upper_set S1 H1 Hyz). 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.