for V being RealLinearSpace
for M being Subset of V holds
( ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) iff M is convex ) by Lm1, Lm2;