proposition: Proposition isaprop_directed_complete_poset {X : hSet} (PX : PartialOrder X) : isaprop (directed_complete_poset PX).
proof: Proof. repeat (use impred ; intro). apply isaprop_lub. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets