let n be Nat; :: thesis: for r being real number
for e being Point of (Euclid n) holds Ball e,r c= OpenHypercube e,r
let r be real number ; :: thesis: for e being Point of (Euclid n) holds Ball e,r c= OpenHypercube e,r
let e be Point of (Euclid n); :: thesis: Ball e,r c= OpenHypercube e,r
let g be set ; :: according to TARSKI:def 3 :: thesis: ( not g in Ball e,r or g in OpenHypercube e,r )
assume A1: g in Ball e,r ; :: thesis: g in OpenHypercube e,r
then reconsider g = g as Point of (Euclid n) ;
A2: dom (Intervals e,r) = dom e by Def3;
A3: ( dom g = Seg n & dom e = Seg n ) by EUCLID:3;

now

let x be set ; :: thesis: ( x in dom (Intervals e,r) implies g . x in (Intervals e,r) . x )
reconsider u = e . x, v = g . x as Real by XREAL_0:def 1;
assume A4: x in dom (Intervals e,r) ; :: thesis: g . x in (Intervals e,r) . x
then A5: (Intervals e,r) . x = ].(u - r),(u + r).[ by A2, Def3;
dom (g - e) = (dom g) /\ (dom e) by VALUED_1:12;
then A6: (g - e) . x = v - u by A2, A3, A4, VALUED_1:13;
A7: v = u + (v - u) ;
abs ((g - e) . x) < r by A1, Th10;
hence g . x in (Intervals e,r) . x by A6, A5, A7, FCONT_3:11; :: thesis: verum

end;

hence g in OpenHypercube e,r by A2, A3, CARD_3:18; :: thesis: verum