let m be non zero Nat; :: thesis: for X being Subset of (REAL m) holds
( X is open iff 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 ) )
let X be Subset of (REAL m); :: thesis: ( X is open iff 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 ) )

hereby :: thesis: ( ( 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 ) ) implies X is open )

assume X is open ; :: thesis: for x being Element of REAL m st x in X holds
ex d0 being Real st
( 0 < d0 & { y where y is Element of REAL m : |.(y - x).| < d0 } c= X )
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: ( x in X implies ex d0 being Real st
( 0 < d0 & { y where y is Element of REAL m : |.(y - x).| < d0 } c= X ) )
assume A2: x in X ; :: thesis: ex d0 being Real st
( 0 < d0 & { y where y is Element of REAL m : |.(y - x).| < d0 } c= X )
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: ( 0 < d0 & { y where y is Element of REAL m : |.(y - x).| < d0 } c= X )
thus 0 < d0 by A3; :: thesis: { y where y is Element of REAL m : |.(y - x).| < d0 } c= X
thus { y where y is Element of REAL m : |.(y - x).| < d0 } c= X :: thesis: verum

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Element of REAL m : |.(y - x).| < d0 } or z in X )
assume z in { y where y is Element of REAL m : |.(y - x).| < d0 } ; :: thesis: z in X
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: verum

end;

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: X is open
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 )

proof

let v be Point of (REAL-NS m); :: thesis: ( v in V0 implies ex r being Real st
( r > 0 & { w where w is Point of (REAL-NS m) : ||.(v - w).|| < r } c= V0 ) )
assume A6: v in V0 ; :: thesis: ex r being Real st
( r > 0 & { w where w is Point of (REAL-NS m) : ||.(v - w).|| < r } c= V0 )
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: ( d0 > 0 & { w where w is Point of (REAL-NS m) : ||.(v - w).|| < d0 } c= V0 )
thus 0 < d0 by A7; :: thesis: { w where w is Point of (REAL-NS m) : ||.(v - w).|| < d0 } c= V0
thus { w where w is Point of (REAL-NS m) : ||.(v - w).|| < d0 } c= V0 :: thesis: verum

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { w where w is Point of (REAL-NS m) : ||.(v - w).|| < d0 } or z in V0 )
assume z in { w where w is Point of (REAL-NS m) : ||.(v - w).|| < d0 } ; :: thesis: z in V0
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: verum

end;

end;

then V0 is open by NORMSP_2:7;
then VV0 is open by NORMSP_2:16;
hence X is open ; :: thesis: verum