theorem :: RLVECT_X:23

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