let n be Nat; :: thesis: for r being real number
for e being Point of (Euclid n) st 0 < r holds
e in OpenHypercube e,r
let r be real number ; :: thesis: for e being Point of (Euclid n) st 0 < r holds
e in OpenHypercube e,r
let e be Point of (Euclid n); :: thesis: ( 0 < r implies e in OpenHypercube e,r )
assume A1: 0 < r ; :: thesis: e in OpenHypercube e,r
set f = Intervals e,r;
A2: dom (Intervals e,r) = dom e by Def3;

now

let x be set ; :: thesis: ( x in dom (Intervals e,r) implies e . x in (Intervals e,r) . x )
assume x in dom (Intervals e,r) ; :: thesis: e . x in (Intervals e,r) . x
then A3: (Intervals e,r) . x = ].((e . x) - r),((e . x) + r).[ by A2, Def3;
A4: (e . x) - r < (e . x) - 0 by A1, XREAL_1:12;
(e . x) + 0 < (e . x) + r by A1, XREAL_1:10;
hence e . x in (Intervals e,r) . x by A3, A4, XXREAL_1:4; :: thesis: verum

end;

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