theorem Th8: :: CONVEX2:8
for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of V