let n be Nat; :: thesis: for r being Real
for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube (e,r) c= Ball (e,(r * (sqrt n)))
let r be Real; :: thesis: for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube (e,r) c= Ball (e,(r * (sqrt n)))
let e be Point of (Euclid n); :: thesis: ( n <> 0 implies OpenHypercube (e,r) c= Ball (e,(r * (sqrt n))) )
assume A1: n <> 0 ; :: thesis: OpenHypercube (e,r) c= Ball (e,(r * (sqrt n)))
then A2: OpenHypercube (e,((r * (sqrt n)) / (sqrt n))) c= Ball (e,(r * (sqrt n))) by Th17;
(r / (sqrt n)) * (sqrt n) = r by A1, XCMPLX_1:87;
hence OpenHypercube (e,r) c= Ball (e,(r * (sqrt n))) by A2, XCMPLX_1:74; :: thesis: verum