intro I1 hI1 I2 hI2 x hx
case refine_1

⊢ ∀ t₁ ∈ lower_intervals, ∀ t₂ ∈ lower_intervals, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
case refine_1
I1 : Set ℝ
hI1 : I1 ∈ lower_intervals
I2 : Set ℝ
hI2 : I2 ∈ lower_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2