consider x being C_Linear_Combination of V;
x in C_LinComb V by Def12;
hence not C_LinComb V is empty ; :: thesis: verum