exact ⟨Sup.sup a c, Inf.inf b d, rfl ⟩
case h.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ∈ lower_intervals
no goals