for x being set
for V being RealLinearSpace
for v being VECTOR of V holds
( x in Lin {v} iff ex a being Real st x = a * v )