∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p : (x : P) → x ∈ affineSpan k s → Prop},
  (∀ (y : P) (hys : y ∈ s), p y ⋯) →
    (∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
        p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯) →
      ∀ {x : P} (h : x ∈ affineSpan k s), p x h