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

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

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

A5: now

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

end;

A18: now

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

end;

A22: 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 A23: 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 that
A24: x in S and
A25: y in S ; :: thesis: dist x,y <= s
S c= CL by A2, A3, PRE_TOPC:48;
hence dist x,y <= s by A23, A24, A25; :: thesis: verum

end;

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

end;

A26: CL <> {} by A2, A3, A4, PCOMPS_1:2;
(diameter S) + 1 > 0 + 0 by A1, TBSP_1:29, XREAL_1:10;
then CL is bounded by A18, TBSP_1:def 9;
hence ( CL is bounded & diameter S = diameter CL ) by A26, A5, A22, 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, A3, PCOMPS_1:2; :: thesis: verum

end;

end;