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 r >= 0 ; :: thesis: p in ClosedHypercube (p,(n |-> r))
then for i being Nat st i in (Seg n) /\ (dom (n |-> r)) holds
(n |-> r) . i >= 0 by FINSEQ_2:57;
hence p in ClosedHypercube (p,(n |-> r)) by Th5; :: thesis: verum