theorem :: RLVECT_4:33
for V being RealLinearSpace
for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds
Lin {v} = Lin {w}