for x being set
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V holds
( x in Z_Lin {v1,v2,v3} iff ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) )