let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for S, CL being Subset of M st S is bounded holds
for S' being Subset of (TopSpaceMetr M) st S = S' & CL = Cl S' holds
( CL is bounded & diameter S = diameter CL )
let S, CL be Subset of M; :: thesis: ( S is bounded implies for S' being Subset of (TopSpaceMetr M) st S = S' & CL = Cl S' holds
( CL is bounded & diameter S = diameter CL ) )
assume A1: S is bounded ; :: thesis: for S' being Subset of (TopSpaceMetr M) st S = S' & CL = Cl S' holds
( CL is bounded & diameter S = diameter CL )
set T = TopSpaceMetr M;
set d = diameter S;
let S' be Subset of (TopSpaceMetr M); :: thesis: ( S = S' & CL = Cl S' implies ( CL is bounded & diameter S = diameter CL ) )
assume A2: ( S = S' & CL = Cl S' ) ; :: thesis: ( CL is bounded & diameter S = diameter CL )

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

suppose A3: S <> {} ; :: thesis: ( CL is bounded & diameter S = diameter CL )

then A4: CL <> {} by A2, PCOMPS_1:2;
A5: (diameter S) + 1 > 0 + 0 by A1, TBSP_1:29, XREAL_1:10;

A6: now

let x, y be Point of M; :: thesis: ( x in CL & y in CL implies not dist x,y > diameter S )
assume A7: ( x in CL & y in CL ) ; :: thesis: not dist x,y > diameter S
assume A8: dist x,y > diameter S ; :: thesis: contradiction
set dxy = dist x,y;
set dd = (dist x,y) - (diameter S);
set dd2 = ((dist x,y) - (diameter S)) / 2;
set Bx = Ball x,(((dist x,y) - (diameter S)) / 2);
set By = Ball y,(((dist x,y) - (diameter S)) / 2);
reconsider BX = Ball x,(((dist x,y) - (diameter S)) / 2), BY = Ball y,(((dist x,y) - (diameter S)) / 2) as Subset of (TopSpaceMetr M) ;
reconsider X = x, Y = y as Point of (TopSpaceMetr M) ;
(dist x,y) - (diameter S) > (diameter S) - (diameter S) by A8, XREAL_1:16;
then A9: ((dist x,y) - (diameter S)) / 2 > 0 / 2 by XREAL_1:76;
( dist x,x = 0 & dist y,y = 0 & Ball x,(((dist x,y) - (diameter S)) / 2) in Family_open_set M & Ball y,(((dist x,y) - (diameter S)) / 2) in Family_open_set M ) by METRIC_1:1, PCOMPS_1:33;
then ( X in BX & Y in BY & BX is open & BY is open ) by A9, METRIC_1:12, PRE_TOPC:def 5;
then A10: ( BX meets S' & BY meets S' ) by A2, A7, TOPS_1:39;
then consider x1 being set such that
A11: ( x1 in BX & x1 in S' ) by XBOOLE_0:3;
consider y1 being set such that
A12: ( y1 in BY & y1 in S' ) by A10, XBOOLE_0:3;
reconsider x1 = x1, y1 = y1 as Point of M by A11, A12;
A13: ( dist x1,y1 <= diameter S & dist x,x1 < ((dist x,y) - (diameter S)) / 2 & dist y,y1 < ((dist x,y) - (diameter S)) / 2 ) by A1, A2, A11, A12, METRIC_1:12, TBSP_1:def 10;
then ( dist x,y1 <= (dist x,x1) + (dist x1,y1) & (dist x,x1) + (dist x1,y1) < (((dist x,y) - (diameter S)) / 2) + (diameter S) & dist y1,y < ((dist x,y) - (diameter S)) / 2 ) by METRIC_1:4, XREAL_1:10;
then dist x,y1 < (((dist x,y) - (diameter S)) / 2) + (diameter S) by XXREAL_0:2;
then ( dist x,y <= (dist x,y1) + (dist y1,y) & (dist x,y1) + (dist y1,y) < ((((dist x,y) - (diameter S)) / 2) + (diameter S)) + (((dist x,y) - (diameter S)) / 2) ) by A13, METRIC_1:4, XREAL_1:10;
hence contradiction ; :: thesis: verum

end;

now

let x, y be Point of M; :: thesis: ( x in CL & y in CL implies dist x,y <= (diameter S) + 1 )
assume A14: ( x in CL & y in CL ) ; :: thesis: dist x,y <= (diameter S) + 1
( dist x,y <= diameter S & (diameter S) + 0 < (diameter S) + 1 ) by A6, A14, XREAL_1:10;
hence dist x,y <= (diameter S) + 1 by XXREAL_0:2; :: thesis: verum

end;

then A15: CL is bounded by A5, TBSP_1:def 9;

now

let s be Real; :: thesis: ( ( for x, y being Point of M st x in CL & y in CL holds
dist x,y <= s ) implies diameter S <= s )
assume A16: for x, y being Point of M st x in CL & y in CL holds
dist x,y <= s ; :: thesis: diameter S <= s

now

let x, y be Point of M; :: thesis: ( x in S & y in S implies dist x,y <= s )
assume A17: ( x in S & y in S ) ; :: thesis: dist x,y <= s
S c= CL by A2, PRE_TOPC:48;
hence dist x,y <= s by A16, A17; :: thesis: verum

end;

hence diameter S <= s by A1, A3, TBSP_1:def 10; :: thesis: verum

end;

hence ( CL is bounded & diameter S = diameter CL ) by A4, A6, A15, TBSP_1:def 10; :: thesis: verum

end;

suppose S = {} ; :: thesis: ( CL is bounded & diameter S = diameter CL )

hence ( CL is bounded & diameter S = diameter CL ) by A2, PCOMPS_1:2; :: thesis: verum

end;

end;