Proposition isaprop_directed_complete_poset {X : hSet} (PX : PartialOrder X) : isaprop (directed_complete_poset PX). Proof. repeat (use impred ; intro). apply isaprop_lub. 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.