for V being RealUnitarySpace
for v, w1, w2 being VECTOR of V
for x being set holds
( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )