let m be non zero Nat; :: thesis:
let X be Subset of (REAL m); :: thesis:

assume X is open ; :: thesis:
then consider VV0 being Subset of (REAL-NS m) such that
A1: ( X = VV0 & VV0 is open ) ;
let x be Element of REAL m; :: thesis:
assume A2: x in X ; :: thesis:
reconsider V0 = VV0 as Subset of (TopSpaceNorm (REAL-NS m)) ;
reconsider v0 = x as Point of (REAL-NS m) by REAL_NS1:def 4;
V0 is open by A1, NORMSP_2:16;
then consider d0 being Real such that
A3: ( d0 > 0 & { w where w is Point of (REAL-NS m) : ||.(v0 - w).|| < d0 } c= V0 ) by A2, A1, NORMSP_2:7;
take d0 = d0; :: thesis:
thus 0 < d0 by A3; :: thesis:
thus { y where y is Element of REAL m : |.(y - x).| < d0 } c= X :: thesis:

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { y where y is Element of REAL m : |.(y - x).| < d0 } ; :: thesis:
then consider y being Element of REAL m such that
A4: ( z = y & |.(y - x).| < d0 ) ;
reconsider w = y as Point of (REAL-NS m) by REAL_NS1:def 4;
|.(y - x).| = ||.(w - v0).|| by REAL_NS1:1, REAL_NS1:5;
then ||.(v0 - w).|| < d0 by A4, NORMSP_1:7;
then w in { w1 where w1 is Point of (REAL-NS m) : ||.(v0 - w1).|| < d0 } ;
hence z in X by A4, A1, A3; :: thesis:

end;

assume A5: for x being Element of REAL m st x in X holds
ex r being Real st
( r > 0 & { y where y is Element of REAL m : |.(y - x).| < r } c= X ) ; :: thesis:
reconsider VV0 = X as Subset of (REAL-NS m) by REAL_NS1:def 4;
reconsider V0 = VV0 as Subset of (TopSpaceNorm (REAL-NS m)) ;
for v being Point of (REAL-NS m) st v in V0 holds
ex r being Real st
( r > 0 & { w where w is Point of (REAL-NS m) : ||.(v - w).|| < r } c= V0 )

let v be Point of (REAL-NS m); :: thesis:
assume A6: v in V0 ; :: thesis:
reconsider x = v as Element of REAL m by REAL_NS1:def 4;
consider d0 being Real such that
A7: ( d0 > 0 & { y where y is Element of REAL m : |.(y - x).| < d0 } c= X ) by A5, A6;
take d0 ; :: thesis:
thus 0 < d0 by A7; :: thesis:
thus { w where w is Point of (REAL-NS m) : ||.(v - w).|| < d0 } c= V0 :: thesis:

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { w where w is Point of (REAL-NS m) : ||.(v - w).|| < d0 } ; :: thesis:
then consider w being Point of (REAL-NS m) such that
A8: ( z = w & ||.(v - w).|| < d0 ) ;
reconsider y = w as Element of REAL m by REAL_NS1:def 4;
|.(y - x).| = ||.(w - v).|| by REAL_NS1:1, REAL_NS1:5;
then |.(y - x).| < d0 by A8, NORMSP_1:7;
then y in { t where t is Element of REAL m : |.(t - x).| < d0 } ;
hence z in V0 by A8, A7; :: thesis:

end;