let n be Nat; :: thesis: for r being Real
for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r)
let r be Real; :: thesis: for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r)
let e be Point of (Euclid n); :: thesis: ( n <> 0 implies OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r) )
assume A1: n <> 0 ; :: thesis: OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenHypercube (e,(r / (sqrt n))) or x in Ball (e,r) )
assume A2: x in OpenHypercube (e,(r / (sqrt n))) ; :: thesis: x in Ball (e,r)
then reconsider x = x as Point of (Euclid n) ;
A3: dist (x,e) < (r / (sqrt n)) * (sqrt n) by A1, A2, Th16;
(r / (sqrt n)) * (sqrt n) = r by A1, XCMPLX_1:87;
hence x in Ball (e,r) by A3, METRIC_1:11; :: thesis: verum