theorem Th11: :: SRINGS_5:14

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