Proposition less_than_dcpo_lub {X : dcpo} (D : directed_set X) (x : X) (i : D) (H : x ⊑ D i) : x ⊑ ⨆ D. Proof. exact (trans_PartialOrder X H (is_least_upperbound_is_upperbound (is_least_upperbound_dcpo_lub D) i)). 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.