fact: Definition way_below {X : dcpo} (x y : X) : hProp := (∀ (D : directed_set X), y ⊑ ⨆ D ⇒ ∃ (i : D), x ⊑ D i)%logic.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics