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