no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
H₁ : Set.Nonempty (Ioi a)
H₂ : a ≤ b
⊢ b ∈ closure (Ioi a)
rwa [closure_Ioi' H₁]