for V being RealLinearSpace
for w1, w2 being VECTOR of V holds w1 in Z_Lin {w1,w2}