let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for r being Real st r >= 0 holds
p in ClosedHypercube (p,(n |-> r))
let p be Point of (TOP-REAL n); :: thesis: for r being Real st r >= 0 holds
p in ClosedHypercube (p,(n |-> r))
let r be Real; :: thesis: ( r >= 0 implies p in ClosedHypercube (p,(n |-> r)) )
set R = n |-> r;
assume A1: r >= 0 ; :: thesis: p in ClosedHypercube (p,(n |-> r))

now :: thesis: for i being Nat st i in (Seg n) /\ (dom (n |-> r)) holds
(n |-> r) . i >= 0

let i be Nat; :: thesis: ( i in (Seg n) /\ (dom (n |-> r)) implies (n |-> r) . i >= 0 )
assume i in (Seg n) /\ (dom (n |-> r)) ; :: thesis: (n |-> r) . i >= 0
then i in Seg n by XBOOLE_0:def 4;
hence (n |-> r) . i >= 0 by FINSEQ_2:57, A1; :: thesis: verum

end;

hence p in ClosedHypercube (p,(n |-> r)) by Th5; :: thesis: verum