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)) ;

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 )

hence P is open by A1, TOPS_3:76; :: thesis: verum

( 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 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 ) 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;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

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

then
P1 is open
by TOPMETR:15;
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;( 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

hence P is open by A1, TOPS_3:76; :: thesis: verum