theorem ThTrivial2: :: ZMODUL07:42

for V being Z_Module
for v being VECTOR of V st v <> 0. V holds
not Lin {v} is trivial