fact: Definition is_directed_complete (P : Poset) : UU := ∏ A : Directed_hsubtype P, least_upper_bound (directed_family A).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.WellOrderedSets UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo