let n be Nat; :: thesis: for r being real number
for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube e,(r / (sqrt n)) c= Ball e,r
let r be real number ; :: 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 set ; :: 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:88;
hence x in Ball e,r by A3, METRIC_1:12; :: thesis: verum