theorem :: TIETZE_2:14

for n being Nat
for p being Point of (TOP-REAL n)
for r, s being Real st r < s holds
ClosedHypercube (p,(n |-> r)) c= OpenHypercube (p,s)