no goals
X : Type u
α : Type v
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s
simpa only [image_id] using hs.intermediate_value ha hb continuousOn_id