theorem :: RLVECT_X:24

for x being set
for V being RealLinearSpace
for v, w1, w2, w3 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2,w3}) iff ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )