theorem Th12: :: SRINGS_5:15

for n being Nat
for r being Real
for p, q being Point of (TOP-REAL n) st q in OpenHypercube (p,(r / 2)) holds
OpenHypercube (q,(r / 2)) c= OpenHypercube (p,r)