let n be Nat; :: thesis: for r being Real
for e being Point of (Euclid n) st 0 < r holds
e in OpenHypercube (e,r)
let r be Real; :: 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 :: thesis: for x being object st x in dom (Intervals (e,r)) holds
e . x in (Intervals (e,r)) . x

let x be object ; :: 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:10;
(e . x) + 0 < (e . x) + r by A1, XREAL_1:8;
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:9; :: thesis: verum