for V being ComplexLinearSpace
for L being C_Linear_Combination of V st L is convex holds
Carrier L <> {}