let n be Element of 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:13;

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 Def2;

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:71;
consider x0 being Element of C;
x0 in C by A1;
then reconsider x0 = x0 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 9;
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:13;
|.(q1 - (0. (TOP-REAL n))).| = dist o,z by JGRAPH_1:45;
then A3: |.q1.| = dist o,z by RLVECT_1:26;
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:8;
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:31;
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

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

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

consider x0 being Element of C;
x0 in C by A6;
then reconsider x0 = x0 as Point of (Euclid n) ;
reconsider q0 = x0 as Point of (TOP-REAL n) by TOPREAL3:13;
reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:71;
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:45
.= |.q2.| by RLVECT_1:26 ;
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:45
.= |.q1.| by RLVECT_1:26 ;
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:9;
hence dist x,y <= r + r by XXREAL_0:2; :: thesis: verum

end;

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

end;

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

hence C is bounded ; :: thesis: verum

end;

end;

end;

hence A is Bounded by Def2; :: thesis: verum