for V being RealLinearSpace
for v, u being VECTOR of V
for A being Subset of V st v in conv A & u in conv A & v <> u holds
ex p, w being VECTOR of V ex r being Real st
( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )