theorem :: RLVECT_4:12

for V being RealLinearSpace
for w1, w2 being VECTOR of V holds
( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )