for V being RealLinearSpace
for L being Linear_Combination of V holds
( L is convex iff ( sum L = 1 & ( for v being VECTOR of V holds 0 <= L . v ) ) )