theorem Th9: :: TIETZE_2:10

for n being Nat
for p, q being Point of (TOP-REAL n)
for R being real-valued FinSequence holds
( q in Fr (ClosedHypercube (p,R)) iff ( q in ClosedHypercube (p,R) & ex i being Nat st
( i in Seg n & ( q . i = (p . i) - (R . i) or q . i = (p . i) + (R . i) ) ) ) )