let n be Nat; :: thesis:
let A be Subset of (TOP-REAL n); :: thesis:
reconsider B = A as Subset of (Euclid n) by TOPREAL3:8;
thus ( A is bounded implies ex p being Point of (Euclid n) ex r being Real st A c= OpenHypercube (p,r) ) :: thesis:

proof

assume A is bounded ; :: thesis:
then A1: B is bounded by JORDAN2C:11;

per cases ;

suppose A2: A is empty ; :: thesis:

take p = the Point of (Euclid n); :: thesis:
take r = the Real; :: thesis:
thus A c= OpenHypercube (p,r) by A2; :: thesis:

end;

suppose not A is empty ; :: thesis:

then consider p being object such that
A3: p in B by XBOOLE_0:def 1;
reconsider p = p as Element of (Euclid n) by A3;
consider r being Real such that
0 < r and
A4: for x, y being Point of (Euclid n) st x in B & y in B holds
dist (x,y) <= r by A1;
take p ; :: thesis:
take r1 = r + 1; :: thesis:
A5: B c= Ball (p,r1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: x in B ; :: thesis:
then reconsider x = x as Element of (Euclid n) ;
dist (p,x) < r1 by A3, A4, A6, XREAL_1:39;
hence x in Ball (p,r1) by METRIC_1:11; :: thesis:

end;

Ball (p,r1) c= OpenHypercube (p,r1) by EUCLID_9:22;
hence A c= OpenHypercube (p,r1) by A5; :: thesis:

end;

end;

end;

given p being Point of (Euclid n), r being Real such that A7: A c= OpenHypercube (p,r) ; :: thesis:

per cases ;

suppose n = 0 ; :: thesis:

then OpenHypercube (p,r) = {{}} by EUCLID_9:12;
then ( B = {} or B = {0} ) by A7, ZFMISC_1:33;
hence A is bounded by JORDAN2C:11; :: thesis:

end;

suppose n <> 0 ; :: thesis:

then OpenHypercube (p,r) c= Ball (p,(r * (sqrt n))) by EUCLID_9:18;
then B is bounded by A7, TBSP_1:14, XBOOLE_1:1;
hence A is bounded by JORDAN2C:11; :: thesis:

end;

end;