let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V st L is convex holds
L <> ZeroLC V
let L be Linear_Combination of V; :: thesis: ( L is convex implies L <> ZeroLC V )
assume A1: L is convex ; :: thesis: L <> ZeroLC V
assume A2: L = ZeroLC V ; :: thesis: contradiction
Carrier L <> {} by A1, Th21;
hence contradiction by A2, RLVECT_2:def 7; :: thesis: verum