proposition: Lemma posetofdcpomorphisms_isdirectedcomplete (D D' : dcpo) : isdirectedcomplete (posetofdcpomorphisms D D').
proof: Proof. intros I F isdirec. exists (make_dcpomorphism (pointwiselub F isdirec) (pointwiselub_isdcpomorphism' F isdirec)). apply pointwiselub_islub. Qed.
imports: UniMath.Foundations.All