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

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