theorem Th8: :: NDIFF_5:8

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