∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p →
    ∀ {w : ι → k} {s : Finset ι},
      ∑ i ∈ s, w i = 1 →
        ∀ {i₁ i₂ i₃ : ι},
          i₁ ∈ s →
            i₂ ∈ s →
              i₃ ∈ s →
                i₁ ≠ i₂ →
                  i₁ ≠ i₃ →
                    i₂ ≠ i₃ →
                      ∀ {c : k},
                        0 < c →
                          c < 1 →
                            (Finset.affineCombination k s p) w ∈
                                affineSpan k {p i₁, (AffineMap.lineMap (p i₂) (p i₃)) c} →
                              SignType.sign (w i₂) = SignType.sign (w i₃)