theorem Th13: :: EUCLID_9:13

for n being Nat
for r, s being Real
for e being Point of (Euclid n) st r <= s holds
OpenHypercube (e,r) c= OpenHypercube (e,s)