let n be Nat; :: thesis: for V being Subset of () st V is open holds
for e being Point of () st e in V holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V )

let V be Subset of (); :: thesis: ( V is open implies for e being Point of () 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 () st e in V holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V )

let e be Point of (); :: 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 ;
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 ;
hence ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V ) by ; :: 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. ();
A9: ( Ball (e,r) = {} or Ball (e,r) = {(0. ())} ) by ;
the carrier of () = the carrier of () by TOPMETR:12;
then OpenHypercube (e,1) = {(0. ())} by ;
hence ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V ) by A9, A2, A3; :: thesis: verum
end;
end;