for n, i being Nat
for p being Point of (TOP-REAL n)
for r being Real st i in Seg n holds
(PROJ (n,i)) .: (OpenHypercube (p,r)) = ].((p . i) - r),((p . i) + r).[