Proposition is_least_upperbound_dcpo_lub {X : dcpo} (D : directed_set X) : is_least_upperbound X D (⨆ D). Proof. apply (pr22 X _ D (directed_set_is_directed D)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.