let n be Nat; :: thesis: for r being Real

for e, e1 being Point of (Euclid n) 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 (Euclid n) 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 (Euclid n); :: 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 (TopSpaceMetr (Euclid n)) ;

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 A1, TOPMETR:15;

for e, e1 being Point of (Euclid n) 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 (Euclid n) 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 (Euclid n); :: 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 (TopSpaceMetr (Euclid n)) ;

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 A1, TOPMETR:15;

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

end;

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 A2, FRECHET:36;

reconsider m = m as non zero Element of NAT by A6, ORDINAL1:def 12;

A7: OpenHypercube (e1,(s / (sqrt n))) c= Ball (e1,s) by A4, Th17;

OpenHypercube (e1,(1 / m)) c= OpenHypercube (e1,(s / (sqrt n))) by A5, Th13;

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 A3, XBOOLE_1:1; :: thesis: verum

end;A5: 1 / m < s / (sqrt n) and

A6: m > 0 by A2, FRECHET:36;

reconsider m = m as non zero Element of NAT by A6, ORDINAL1:def 12;

A7: OpenHypercube (e1,(s / (sqrt n))) c= Ball (e1,s) by A4, Th17;

OpenHypercube (e1,(1 / m)) c= OpenHypercube (e1,(s / (sqrt n))) by A5, Th13;

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 A3, XBOOLE_1:1; :: thesis: verum

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 A1, EUCLID:77, ZFMISC_1:33;

hence ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) ; :: thesis: verum

end;hence ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) ; :: thesis: verum