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 L is convex ; :: thesis: L <> ZeroLC V
then A1: Carrier L <> {} by Th21;
assume L = ZeroLC V ; :: thesis: contradiction
hence contradiction by A1, RLVECT_2:def 5; :: thesis: verum