let n be Nat; :: thesis:
let A be Subset of (TOP-REAL n); :: thesis:
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:

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

A1: now :: thesis:

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

end;

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

end;

assume conv A is bounded ; :: thesis:
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: