for X being LinearTopSpace
for x, v being Point of X
for V being a_neighborhood of x holds v + V is a_neighborhood of v + x