diff --git a/Mathlib/Order/Bounds/Basic.lean b/Mathlib/Order/Bounds/Basic.lean
index 12fbb67bd29471..ceab07c64f1ada 100644
--- a/Mathlib/Order/Bounds/Basic.lean
+++ b/Mathlib/Order/Bounds/Basic.lean
@@ -596,9 +596,11 @@ end
 theorem bddBelow_iff_subset_Ici : BddBelow s ↔ ∃ a, s ⊆ Ici a :=
   Iff.rfl
 
-theorem bddBelow_bddAbove_iff_subset_Icc : BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b := by
-  simp [Ici_inter_Iic.symm, subset_inter_iff, bddBelow_iff_subset_Ici,
-    bddAbove_iff_subset_Iic, exists_and_left, exists_and_right]
+theorem subset_Icc_iff : s ⊆ Icc a b ↔ a ∈ lowerBounds s ∧ b ∈ upperBounds s :=
+   subset_inter_iff.trans (mem_lowerBounds_iff_subset_Ici.and mem_upperBounds_iff_subset_Iic)
+
+theorem bddBelow_bddAbove_iff_subset_Icc : BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b :=
+  exists_and_exists_comm.trans <| exists₂_congr fun _ _ ↦ subset_Icc_iff.symm
 
 /-!
 #### Univ
diff --git a/Mathlib/Order/Interval/Set/OrdConnected.lean b/Mathlib/Order/Interval/Set/OrdConnected.lean
index 47cae5ddfedfa6..0730b1d17e4f53 100644
--- a/Mathlib/Order/Interval/Set/OrdConnected.lean
+++ b/Mathlib/Order/Interval/Set/OrdConnected.lean
@@ -64,6 +64,10 @@ protected theorem Icc_subset (s : Set α) [hs : OrdConnected s] {x y} (hx : x 
     Icc x y ⊆ s :=
   hs.out hx hy
 
+theorem OrdConnected.eq_Icc {a b : α} (hs : OrdConnected s) (ha : IsLeast s a)
+  (hb : IsGreatest s b) : s = Icc a b :=
+  (subset_Icc_iff.mpr ⟨ha.2, hb.2⟩).antisymm (hs.out ha.1 hb.1)
+
 end Preorder
 
 end Set