for S being RealNormSpace
for x0 being Point of S
for N being Neighbourhood of x0 holds x0 in N