let m be Nat; :: thesis: for P being Subset of () holds
( P is open iff for p being Point of () st p in P holds
ex r being positive Real st Ball (p,r) c= P )

let P be Subset of (); :: thesis: ( P is open iff for p being Point of () st p in P holds
ex r being positive Real st Ball (p,r) c= P )

A1: TopStruct(# the U1 of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider P1 = P as Subset of () ;
hereby :: thesis: ( ( for p being Point of () 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 () st p in P holds
ex r being positive Real st Ball (p,r) c= P

let p be Point of (); :: 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 () by EUCLID:67;
P1 is open by ;
then consider r being Real such that
A4: r > 0 and
A5: Ball (e,r) c= P1 by ;
reconsider r = r as positive Real by A4;
take r = r; :: thesis: Ball (p,r) c= P
thus Ball (p,r) c= P by ; :: thesis: verum
end;
assume A6: for p being Point of () 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 () st p in P1 holds
ex r being Real st
( r > 0 & Ball (p,r) c= P1 )
proof
let p be Point of (); :: 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 () 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 ; :: thesis: verum
end;
then P1 is open by TOPMETR:15;
hence P is open by ; :: thesis: verum