lemma uniq_supremum:
∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
- t1 is_upper_bound s → t2 is_upper_bound s → t1 ≈ t2.
-intros (O s t1 t2 Ht1 Ht2); apply le_le_eq; cases Ht1; cases Ht2;
+ t1 is_strong_sup s → t2 is_strong_sup s → t1 ≈ t2.
+intros (O s t1 t2 Ht1 Ht2); cases Ht1 (U1 H1); cases Ht2 (U2 H2);
+apply le_le_eq; intro X;
+[1: cases (H1 ? X); apply (U2 w); assumption
+|2: cases (H2 ? X); apply (U1 w); assumption]
+qed.
+
+