obtain ⟨y, hy⟩ := hAnemp
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
hAnemp : (interior s).Nonempty
x : E
hx : x ∈ closure s
⊢ x ∈ closure (interior s)
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x : E
hx : x ∈ closure s
y : E
hy : y ∈ interior s
⊢ x ∈ closure (interior s)