∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] {s : Set V} {x y : V},
  x ∉ (convexHull ℝ) s →
    y ∈ (convexHull ℝ) s →
      IsVisible ℝ ((convexHull ℝ) s) x y → y ∈ (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}