Definition make_dcpo_lub_islub {D : dcpo} {I : UU} {f : I -> D} (isdirec : isdirected f) : islub f (make_dcpo_lub isdirec). Proof. exact (pr2 (dcpoisdirectedcomplete D I f isdirec)). Defined.
Require Import UniMath.Foundations.All.