proposition: Lemma isaprop_preserveslub {P Q : Poset} (f : P -> Q) {I : UU} (u : I -> P) : isaprop (preserveslub f u).
proof: Proof. apply impred_isaprop; intro v. apply isapropimpl. apply isaprop_islub. Qed.
imports: UniMath.Foundations.All