let n be Nat; :: thesis: for A being Subset of (TOP-REAL n) holds
( A is bounded iff ex r being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r )
let A be Subset of (TOP-REAL n); :: thesis: ( A is bounded iff ex r being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r )
reconsider C = A as Subset of (Euclid n) by TOPREAL3:8;

hereby :: thesis: ( ex r being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r implies A is bounded )

assume A is bounded ; :: thesis: ex r2 being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r2
then reconsider C = A as bounded Subset of (Euclid n) by Th5;

per cases ( C <> {} or C = {} ) ;

suppose A1: C <> {} ; :: thesis: ex r2 being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r2

reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
set x0 = the Element of C;
the Element of C in C by A1;
then reconsider x0 = the Element of C as Point of (Euclid n) ;
consider r being Real such that
0 < r and
A2: for x, y being Point of (Euclid n) st x in C & y in C holds
dist (x,y) <= r by TBSP_1:def 7;
set R0 = (r + (dist (o,x0))) + 1;
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < (r + (dist (o,x0))) + 1

proof

let q1 be Point of (TOP-REAL n); :: thesis: ( q1 in A implies |.q1.| < (r + (dist (o,x0))) + 1 )
reconsider z = q1 as Point of (Euclid n) by TOPREAL3:8;
|.(q1 - (0. (TOP-REAL n))).| = dist (o,z) by JGRAPH_1:28;
then A3: |.q1.| = dist (o,z) by RLVECT_1:13;
assume q1 in A ; :: thesis: |.q1.| < (r + (dist (o,x0))) + 1
then dist (x0,z) <= r by A2;
then ( dist (o,z) <= (dist (o,x0)) + (dist (x0,z)) & (dist (o,x0)) + (dist (x0,z)) <= (dist (o,x0)) + r ) by METRIC_1:4, XREAL_1:6;
then A4: dist (o,z) <= (dist (o,x0)) + r by XXREAL_0:2;
r + (dist (o,x0)) < (r + (dist (o,x0))) + 1 by XREAL_1:29;
hence |.q1.| < (r + (dist (o,x0))) + 1 by A3, A4, XXREAL_0:2; :: thesis: verum

end;

hence ex r2 being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r2 ; :: thesis: verum

end;

suppose C = {} ; :: thesis: ex r2 being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r2

then for q being Point of (TOP-REAL n) st q in A holds
|.q.| < 1 ;
hence ex r2 being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r2 ; :: thesis: verum

end;

end;

end;

given r being Real such that A5: for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r ; :: thesis: A is bounded

now :: thesis: C is bounded

per cases ( C <> {} or C = {} ) ;

suppose A6: C <> {} ; :: thesis: C is bounded

set x0 = the Element of C;
the Element of C in C by A6;
then reconsider x0 = the Element of C as Point of (Euclid n) ;
reconsider q0 = x0 as Point of (TOP-REAL n) by TOPREAL3:8;
reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
set R0 = r + r;
A7: for x, y being Point of (Euclid n) st x in C & y in C holds
dist (x,y) <= r + r

proof

let x, y be Point of (Euclid n); :: thesis: ( x in C & y in C implies dist (x,y) <= r + r )
assume that
A8: x in C and
A9: y in C ; :: thesis: dist (x,y) <= r + r
reconsider q2 = y as Point of (TOP-REAL n) by A9;
dist (o,y) = |.(q2 - (0. (TOP-REAL n))).| by JGRAPH_1:28
.= |.q2.| by RLVECT_1:13 ;
then A10: dist (o,y) < r by A5, A9;
reconsider q1 = x as Point of (TOP-REAL n) by A8;
dist (x,o) = |.(q1 - (0. (TOP-REAL n))).| by JGRAPH_1:28
.= |.q1.| by RLVECT_1:13 ;
then dist (x,o) < r by A5, A8;
then ( dist (x,y) <= (dist (x,o)) + (dist (o,y)) & (dist (x,o)) + (dist (o,y)) <= r + r ) by A10, METRIC_1:4, XREAL_1:7;
hence dist (x,y) <= r + r by XXREAL_0:2; :: thesis: verum

end;

|.q0.| < r by A5, A6;
hence C is bounded by A7; :: thesis: verum

end;

suppose C = {} ; :: thesis: C is bounded

hence C is bounded ; :: thesis: verum

end;

end;

end;

hence A is bounded by Th5; :: thesis: verum