for S being RealNormSpace
for x being Point of S
for N1, N2 being Neighbourhood of x holds N1 /\ N2 is Neighbourhood of x