theorem Th4: :: NFCONT_1:4

for S being RealNormSpace
for x0 being Point of S
for N being Neighbourhood of x0 holds x0 in N