:: deftheorem defines OpenHypercube EUCLID_9:def 4 :
for n being Nat
for e being Point of (Euclid n)
for r being Real holds OpenHypercube (e,r) = product (Intervals (e,r));