let n be Nat; :: thesis: for V being Subset of (TopSpaceMetr (Euclid n)) st V is open holds

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

ex r being Real st

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

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

ex r being Real st

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

assume A1: V is open ; :: 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 )

let e be Point of (Euclid n); :: thesis: ( e in V implies ex r being Real st

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

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

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

then consider r being Real such that

A2: r > 0 and

A3: Ball (e,r) c= V by A1, TOPMETR:15;

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

ex r being Real st

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

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

ex r being Real st

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

assume A1: V is open ; :: 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 )

let e be Point of (Euclid n); :: thesis: ( e in V implies ex r being Real st

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

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

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

then consider r being Real such that

A2: r > 0 and

A3: Ball (e,r) c= V by A1, TOPMETR:15;

per cases
( n <> 0 or n = 0 )
;

end;

suppose A4:
n <> 0
; :: thesis: ex r being Real st

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

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

OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r)
by A4, EUCLID_9:17;

hence ex r being Real st

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

end;hence ex r being Real st

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

suppose A6:
n = 0
; :: thesis: ex r being Real st

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

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

set TR = TOP-REAL 0;

set Z = 0. (TOP-REAL 0);

A9: ( Ball (e,r) = {} or Ball (e,r) = {(0. (TOP-REAL 0))} ) by EUCLID:77, ZFMISC_1:33, A6;

the carrier of (TopSpaceMetr (Euclid 0)) = the carrier of (Euclid 0) by TOPMETR:12;

then OpenHypercube (e,1) = {(0. (TOP-REAL 0))} by EUCLID:77, ZFMISC_1:33, A6;

hence ex r being Real st

( r > 0 & OpenHypercube (e,r) c= V ) by A9, A2, A3; :: thesis: verum

end;set Z = 0. (TOP-REAL 0);

A9: ( Ball (e,r) = {} or Ball (e,r) = {(0. (TOP-REAL 0))} ) by EUCLID:77, ZFMISC_1:33, A6;

the carrier of (TopSpaceMetr (Euclid 0)) = the carrier of (Euclid 0) by TOPMETR:12;

then OpenHypercube (e,1) = {(0. (TOP-REAL 0))} by EUCLID:77, ZFMISC_1:33, A6;

hence ex r being Real st

( r > 0 & OpenHypercube (e,r) c= V ) by A9, A2, A3; :: thesis: verum