for V being RealLinearSpace
for M being non empty Subset of V
for L1, L2 being Convex_Combination of M
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of M