let n be Nat; :: thesis: for V being Subset of (TopSpaceMetr (Euclid n)) st ( for e being Point of (Euclid n) st e in V holds

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= V ) ) holds

V is open

let V be Subset of (TopSpaceMetr (Euclid n)); :: thesis: ( ( for e being Point of (Euclid n) st e in V holds

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= V ) ) implies V is open )

assume A1: for e being Point of (Euclid n) st e in V holds

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= V ) ; :: thesis: V is open

for e being Point of (Euclid n) st e in V holds

ex r being Real st

( r > 0 & Ball (e,r) c= V )

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= V ) ) holds

V is open

let V be Subset of (TopSpaceMetr (Euclid n)); :: thesis: ( ( for e being Point of (Euclid n) st e in V holds

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= V ) ) implies V is open )

assume A1: for e being Point of (Euclid n) st e in V holds

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= V ) ; :: thesis: V is open

for e being Point of (Euclid n) st e in V holds

ex r being Real st

( r > 0 & Ball (e,r) c= V )

proof

hence
V is open
by TOPMETR:15; :: thesis: verum
let e be Point of (Euclid n); :: thesis: ( e in V implies ex r being Real st

( r > 0 & Ball (e,r) c= V ) )

assume e in V ; :: thesis: ex r being Real st

( r > 0 & Ball (e,r) c= V )

then consider r being Real such that

A2: r > 0 and

A3: OpenHypercube (e,r) c= V by A1;

Ball (e,r) c= OpenHypercube (e,r) by Th22;

hence ex r being Real st

( r > 0 & Ball (e,r) c= V ) by A2, A3, XBOOLE_1:1; :: thesis: verum

end;( r > 0 & Ball (e,r) c= V ) )

assume e in V ; :: thesis: ex r being Real st

( r > 0 & Ball (e,r) c= V )

then consider r being Real such that

A2: r > 0 and

A3: OpenHypercube (e,r) c= V by A1;

Ball (e,r) c= OpenHypercube (e,r) by Th22;

hence ex r being Real st

( r > 0 & Ball (e,r) c= V ) by A2, A3, XBOOLE_1:1; :: thesis: verum