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 real positive number 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 real positive number 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)) ;
A2: m in NAT by ORDINAL1:def 12;

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

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

end;

assume A7: for p being Point of (TOP-REAL m) st p in P holds
ex r being real positive number 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 number 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 number st
( r > 0 & Ball (p,r) c= P1 ) )
assume A8: p in P1 ; :: thesis: ex r being real number st
( r > 0 & Ball (p,r) c= P1 )
reconsider e = p as Point of (TOP-REAL m) by EUCLID:67;
consider r being real positive number such that
A9: Ball (e,r) c= P1 by A7, A8;
take r ; :: thesis: ( r > 0 & Ball (p,r) c= P1 )
thus ( r > 0 & Ball (p,r) c= P1 ) by A2, A9, TOPREAL9:13; :: thesis: verum

end;

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