let m be Nat; :: thesis: for P being Subset of (TOP-REAL m) holds
( P is open iff for p being Point of (TOP-REAL m) st p in P holds
ex r being positive Real st Ball (p,r) c= P )
let P be Subset of (TOP-REAL m); :: thesis: ( P is open iff for p being Point of (TOP-REAL m) st p in P holds
ex r being positive Real st Ball (p,r) c= P )
A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def 8;
then reconsider P1 = P as Subset of (TopSpaceMetr (Euclid m)) ;

hereby :: thesis: ( ( for p being Point of (TOP-REAL m) st p in P holds
ex r being positive Real st Ball (p,r) c= P ) implies P is open )

assume A2: P is open ; :: thesis: for p being Point of (TOP-REAL m) st p in P holds
ex r being positive Real st Ball (p,r) c= P
let p be Point of (TOP-REAL m); :: thesis: ( p in P implies ex r being positive Real st Ball (p,r) c= P )
assume A3: p in P ; :: thesis: ex r being positive Real st Ball (p,r) c= P
reconsider e = p as Point of (Euclid m) by EUCLID:67;
P1 is open by A2, A1, TOPS_3:76;
then consider r being Real such that
A4: r > 0 and
A5: Ball (e,r) c= P1 by A3, TOPMETR:15;
reconsider r = r as positive Real by A4;
take r = r; :: thesis: Ball (p,r) c= P
thus Ball (p,r) c= P by A5, TOPREAL9:13; :: thesis: verum

end;

assume A6: for p being Point of (TOP-REAL m) st p in P holds
ex r being positive Real st Ball (p,r) c= P ; :: thesis: P is open
for p being Point of (Euclid m) st p in P1 holds
ex r being Real st
( r > 0 & Ball (p,r) c= P1 )

proof

let p be Point of (Euclid m); :: thesis: ( p in P1 implies ex r being Real st
( r > 0 & Ball (p,r) c= P1 ) )
assume A7: p in P1 ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= P1 )
reconsider e = p as Point of (TOP-REAL m) by EUCLID:67;
consider r being positive Real such that
A8: Ball (e,r) c= P1 by A6, A7;
take r ; :: thesis: ( r > 0 & Ball (p,r) c= P1 )
thus ( r > 0 & Ball (p,r) c= P1 ) by A8, TOPREAL9:13; :: thesis: verum

end;

then P1 is open by TOPMETR:15;
hence P is open by A1, TOPS_3:76; :: thesis: verum