theorem Th23: :: PDIFF_6:23

for m being Nat
for x0 being Element of REAL m
for y0 being Point of (REAL-NS m)
for r being Real st x0 = y0 holds
{ y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r }