proposition: Lemma is_hausdorff_separated_le (x y z : X) : y ⊑ z → is_hausdorff_separated y x → is_hausdorff_separated z x.
proof: 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.
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