let V be ComplexLinearSpace; :: thesis: for L being C_Linear_Combination of V st L is convex holds
L <> ZeroCLC V
let L be C_Linear_Combination of V; :: thesis: ( L is convex implies L <> ZeroCLC V )
assume L is convex ; :: thesis: L <> ZeroCLC V
then A1: Carrier L <> {} by Th77;
assume L = ZeroCLC V ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum