intro y hy
case h.right.right
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) ⊆ I1 ∩ I2
case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
y : ℝ
hy : y ∈ Set.Ico (a ⊔ c) (b ⊓ d)
⊢ y ∈ I1 ∩ I2