for V being ComplexLinearSpace
for v1, v2 being VECTOR of V
for L being C_Linear_Combination of {v1,v2} st v1 <> v2 & L is convex holds
( ex r1, r2 being Real st
( r1 = L . v1 & r2 = L . v2 & r1 >= 0 & r2 >= 0 ) & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )