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;

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

hence
e in OpenHypercube (e,r)
by A2, CARD_3:9; :: thesis: verume . 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;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