by_contra! h
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ (convexHull 𝕜) s → ∀ ⦃x₂ : E⦄, x₂ ∈ (convexHull 𝕜) s → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
h : ∃ x₁ ∈ (convexHull 𝕜) s, ∃ x₂ ∈ (convexHull 𝕜) s, x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ False