let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for r being Real holds OpenHypercube (p,r) c= ClosedHypercube (p,(n |-> r))
let p be Point of (TOP-REAL n); :: thesis: for r being Real holds OpenHypercube (p,r) c= ClosedHypercube (p,(n |-> r))
let r be Real; :: thesis: OpenHypercube (p,r) c= ClosedHypercube (p,(n |-> r))
set TR = TOP-REAL n;

per cases ( n = 0 or n > 0 ) ;

suppose A1: n = 0 ; :: thesis: OpenHypercube (p,r) c= ClosedHypercube (p,(n |-> r))

then for i being Nat st i in Seg n holds
(0. (TOP-REAL n)) . i in [.((p . i) - ((n |-> r) . i)),((p . i) + ((n |-> r) . i)).] ;
then A2: 0. (TOP-REAL n) in ClosedHypercube (p,(n |-> r)) by Def2;
the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by JORDAN2C:105, A1, EUCLID:22;
then ClosedHypercube (p,(n |-> r)) = [#] (TOP-REAL n) by A2, ZFMISC_1:33;
hence OpenHypercube (p,r) c= ClosedHypercube (p,(n |-> r)) ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: OpenHypercube (p,r) c= ClosedHypercube (p,(n |-> r))

then rng (n |-> r) = {r} by FUNCOP_1:8;
then A3: inf (rng (n |-> r)) = r by XXREAL_2:13;
len (n |-> r) = n by CARD_1:def 7;
hence OpenHypercube (p,r) c= ClosedHypercube (p,(n |-> r)) by Th8, A3; :: thesis: verum

end;

end;