let n be Nat; :: thesis: for r being Real
for e, e1 being Point of () st e1 in Ball (e,r) holds
ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)

let r be Real; :: thesis: for e, e1 being Point of () st e1 in Ball (e,r) holds
ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)

let e, e1 be Point of (); :: thesis: ( e1 in Ball (e,r) implies ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) )
reconsider B = Ball (e,r) as Subset of () ;
assume A1: e1 in Ball (e,r) ; :: thesis: ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)
B is open by TOPMETR:14;
then consider s being Real such that
A2: s > 0 and
A3: Ball (e1,s) c= B by ;
per cases ( n <> 0 or n = 0 ) ;
suppose A4: n <> 0 ; :: thesis: ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)
then consider m being Nat such that
A5: 1 / m < s / (sqrt n) and
A6: m > 0 by ;
reconsider m = m as non zero Element of NAT by ;
A7: OpenHypercube (e1,(s / (sqrt n))) c= Ball (e1,s) by ;
OpenHypercube (e1,(1 / m)) c= OpenHypercube (e1,(s / (sqrt n))) by ;
then OpenHypercube (e1,(1 / m)) c= Ball (e1,s) by A7;
hence ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) by ; :: thesis: verum
end;
suppose n = 0 ; :: thesis: ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)
then ( ( OpenHypercube (e1,(1 / 1)) = {} or OpenHypercube (e1,(1 / 1)) = ) & Ball (e,r) = ) by ;
hence ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) ; :: thesis: verum
end;
end;