theorem :: RUSUB_3:33

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