for n being Nat
for A being Subset of (TOP-REAL n) holds
( A is bounded iff ex p being Point of (Euclid n) ex r being Real st A c= OpenHypercube (p,r) )