∀ (𝕜 : Type u_2) {E : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (x y x_1 : E) (motive : x_1 ∈ segment 𝕜 x y → Prop) (x_2 : x_1 ∈ segment 𝕜 x y),
  (∀ (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (H : a • x + b • y = x_1), motive ⋯) → motive x_2