theorem Th4: :: NFCONT_4:4

for n being Element of NAT
for r being Real
for z being Element of REAL n
for w being Point of (REAL-NS n) st z = w holds
{ y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r }