theorem Th4: :: TIETZE_2:5

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