for N being RealNormSpace
for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds Balls x is basis of (BOOL2F (NeighborhoodSystem x)) by Th5;