let n be Element of NAT ; :: thesis: 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 }
let r be Real; :: thesis: 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 }
let z be Element of REAL n; :: thesis: 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 }
let w be Point of (REAL-NS n); :: thesis: ( z = w implies { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } )
assume A1: z = w ; :: thesis: { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r }
set N1 = { y where y is Element of REAL n : |.(y - z).| < r } ;
set N2 = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } ;
A2: { y where y is Element of REAL n : |.(y - z).| < r } c= { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Element of REAL n : |.(y - z).| < r } or x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } )
assume x in { y where y is Element of REAL n : |.(y - z).| < r } ; :: thesis: x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r }
then consider y being Element of REAL n such that
A3: ( x = y & |.(y - z).| < r ) ;
reconsider x1 = x as Element of REAL n by A3;
reconsider x2 = x1 as Point of (REAL-NS n) by REAL_NS1:def 4;
||.(x2 - w).|| < r by A1, A3, REAL_NS1:1, REAL_NS1:5;
hence x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } ; :: thesis: verum

end;

{ y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } c= { y where y is Element of REAL n : |.(y - z).| < r }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } or x in { y where y is Element of REAL n : |.(y - z).| < r } )
assume x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } ; :: thesis: x in { y where y is Element of REAL n : |.(y - z).| < r }
then consider y being Point of (REAL-NS n) such that
A4: ( x = y & ||.(y - w).|| < r ) ;
reconsider x3 = x as Point of (REAL-NS n) by A4;
reconsider x4 = x3 as Element of REAL n by REAL_NS1:def 4;
|.(x4 - z).| < r by A1, A4, REAL_NS1:1, REAL_NS1:5;
hence x in { y where y is Element of REAL n : |.(y - z).| < r } ; :: thesis: verum

end;

hence { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } by A2, XBOOLE_0:def 10; :: thesis: verum