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 A1:
L is convex
; :: thesis: L <> ZeroCLC V
assume A2:
L = ZeroCLC V
; :: thesis: contradiction
Carrier L <> {}
by A1, Th221;
hence
contradiction
by A2; :: thesis: verum