theorem Th8: :: RLVECT_3:8
for V being RealLinearSpace
for v being VECTOR of V holds
( {v} is linearly-independent iff v <> 0. V )