for S being RealNormSpace
for x0 being Point of S
for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st
( N c= N1 & N c= N2 )