for S being RealNormSpace
for x0 being Point of S
for g being Real st 0 < g holds
{ y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0