Proposition way_below_to_le {x y : X} (p : x ≪ y) : x ⊑ y. Proof. pose (D := nat_directed_set X (λ _, y) (λ _, refl_dcpo _)). assert (q : y ⊑ ⨆ D). { exact (less_than_dcpo_lub D y 0 (refl_dcpo _)). } assert (H := way_below_elem p D q). revert H. use factor_through_squash. { apply propproperty. } intros H. exact (pr2 H). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics.