proposition: Lemma isaprop_isdirectedcomplete (X : Poset) : isaprop (isdirectedcomplete X).
proof: Proof. apply impred_isaprop; intro I. apply impred_isaprop; intro f. apply isapropimpl. apply invproofirrelevance. intros [u p] [v q]. apply total2_paths_equiv. exists (lubsareunique _ p q). apply proofirrelevance. apply isaprop_islub. Qed.
imports: UniMath.Foundations.All