no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
a✝ b✝ : α
inst✝ : TopologicalSpace γ
a b c : α
H : b ∈ Ico a c
⊢ Iio c ∩ Ici b ⊆ Ico a c
simp only [inter_comm, Ici_inter_Iio, Ico_subset_Ico_left H.1]