α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : OrdConnected s
⊢ OrdConnected (interior ↑(upperClosure s) ∩ interior ↑(lowerClosure s))
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : OrdConnected s
⊢ OrdConnected (interior s)
rw [← h.upperClosure_inter_lowerClosure, interior_inter]
no goals
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : OrdConnected s
⊢ OrdConnected (interior ↑(upperClosure s) ∩ interior ↑(lowerClosure s))
exact
  (upperClosure s).upper.interior.ordConnected.inter (lowerClosure s).lower.interior.ordConnected