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;

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

suppose A4: n <> 0 ; :: thesis: ex r being Real st
( 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;

suppose A6: n = 0 ; :: thesis: ex r being Real st
( 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;

end;