let n be Nat; 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; 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); ( n <> 0 implies OpenHypercube (e,r) c= Ball (e,(r * (sqrt n))) )
assume A1:
n <> 0
; 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; verum