for R being Ring
for V being LeftMod of R
for v being Vector of V st v <> 0. V holds
not Lin {v} is trivial