let n be Nat; :: thesis: for A being Subset of (TOP-REAL n) holds
( A is bounded iff conv A is bounded )
let A be Subset of (TOP-REAL n); :: thesis: ( A is bounded iff conv A is bounded )
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider cA = conv A, a = A as Subset of (Euclid n) ;

hereby :: thesis: ( conv A is bounded implies A is bounded )

assume A is bounded ; :: thesis: conv A is bounded
then reconsider a = a as bounded Subset of (Euclid n) by JORDAN2C:11;
set D = diameter a;

A1: now :: thesis: for x, y being Point of (Euclid n) st x in cA & y in cA holds
dist (x,y) <= (diameter a) + 1

let x, y be Point of (Euclid n); :: thesis: ( x in cA & y in cA implies dist (x,y) <= (diameter a) + 1 )
assume x in cA ; :: thesis: ( y in cA implies dist (x,y) <= (diameter a) + 1 )
then A2: conv A c= cl_Ball (x,(diameter a)) by Th13;
assume y in cA ; :: thesis: dist (x,y) <= (diameter a) + 1
then dist (x,y) <= diameter a by A2, METRIC_1:12;
hence dist (x,y) <= (diameter a) + 1 by XREAL_1:39; :: thesis: verum

end;

diameter a >= 0 by TBSP_1:21;
then cA is bounded by A1;
hence conv A is bounded by JORDAN2C:11; :: thesis: verum

end;

assume conv A is bounded ; :: thesis: A is bounded
then cA is bounded by JORDAN2C:11;
then a is bounded by CONVEX1:41, TBSP_1:14;
hence A is bounded by JORDAN2C:11; :: thesis: verum