Definition way_below_principal_incl {X : dcpo} (x : X) : ↡ x → X := pr1.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics.