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