theorem Th5: :: TIETZE_2:6

for n being Nat
for p being Point of (TOP-REAL n)
for R being real-valued FinSequence st ( for i being Nat st i in (Seg n) /\ (dom R) holds
R . i >= 0 ) holds
p in ClosedHypercube (p,R)