Lemma lubsareunique {u v : X} : islub u -> islub v -> u = v. Proof. intros islubu islubv. apply isantisymm_posetRelation. - apply (islub_isleast islubu). exact (islub_isupperbound islubv). - apply (islub_isleast islubv). exact (islub_isupperbound islubu). Qed.
Require Import UniMath.Foundations.All.