for E being RealNormSpace
for x, b being Point of E
for N being Neighbourhood of x holds
( { (z - b) where z is Point of E : z in N } is Neighbourhood of x - b & { (z + b) where z is Point of E : z in N } is Neighbourhood of x + b )