let m be Nat; :: thesis: 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 }
let x0 be Element of REAL m; :: thesis: 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 }
let y0 be Point of (REAL-NS m); :: thesis: 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 }
let r be Real; :: thesis: ( x0 = y0 implies { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } )
assume A1: x0 = y0 ; :: thesis: { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r }

now :: thesis: for w being object st w in { y where y is Element of REAL m : |.(y - x0).| < r } holds
w in { z1 where z1 is Point of (REAL-NS m) : ||.(z1 - y0).|| < r }

let w be object ; :: thesis: ( w in { y where y is Element of REAL m : |.(y - x0).| < r } implies w in { z1 where z1 is Point of (REAL-NS m) : ||.(z1 - y0).|| < r } )
assume w in { y where y is Element of REAL m : |.(y - x0).| < r } ; :: thesis: w in { z1 where z1 is Point of (REAL-NS m) : ||.(z1 - y0).|| < r }
then consider y being Element of REAL m such that
A2: ( y = w & |.(y - x0).| < r ) ;
reconsider z = y as Point of (REAL-NS m) by REAL_NS1:def 4;
||.(z - y0).|| < r by A1, A2, REAL_NS1:1, REAL_NS1:5;
hence w in { z1 where z1 is Point of (REAL-NS m) : ||.(z1 - y0).|| < r } by A2; :: thesis: verum

end;

then A3: { y where y is Element of REAL m : |.(y - x0).| < r } c= { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } by TARSKI:def 3;

now :: thesis: for w being object st w in { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } holds
w in { z1 where z1 is Element of REAL m : |.(z1 - x0).| < r }

let w be object ; :: thesis: ( w in { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } implies w in { z1 where z1 is Element of REAL m : |.(z1 - x0).| < r } )
assume w in { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } ; :: thesis: w in { z1 where z1 is Element of REAL m : |.(z1 - x0).| < r }
then consider y being Point of (REAL-NS m) such that
A4: ( y = w & ||.(y - y0).|| < r ) ;
reconsider z = y as Element of REAL m by REAL_NS1:def 4;
|.(z - x0).| < r by A1, A4, REAL_NS1:1, REAL_NS1:5;
hence w in { z1 where z1 is Element of REAL m : |.(z1 - x0).| < r } by A4; :: thesis: verum

end;

then { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } c= { y where y is Element of REAL m : |.(y - x0).| < r } by TARSKI:def 3;
hence { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } by A3, XBOOLE_0:def 10; :: thesis: verum