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 :: thesis: for x, y being Point of M st x in CL & y in CL holds
not dist (x,y) > diameter S

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:14;
then A8: ((dist (x,y)) - (diameter S)) / 2 > 0 / 2 by XREAL_1:74;
Ball (y,(((dist (x,y)) - (diameter S)) / 2)) in Family_open_set M by PCOMPS_1:29;
then A9: BY is open by PRE_TOPC:def 2;
Ball (x,(((dist (x,y)) - (diameter S)) / 2)) in Family_open_set M by PCOMPS_1:29;
then A10: BX is open by PRE_TOPC:def 2;
dist (y,y) = 0 by METRIC_1:1;
then Y in BY by A8, METRIC_1:11;
then BY meets S9 by A3, A7, A9, TOPS_1:12;
then consider y1 being object 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:11;
then BX meets S9 by A3, A6, A10, TOPS_1:12;
then consider x1 being object 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:11;
dist (x1,y1) <= diameter S by A1, A2, A14, A12, TBSP_1:def 8;
then A16: (dist (x,x1)) + (dist (x1,y1)) < (((dist (x,y)) - (diameter S)) / 2) + (diameter S) by A15, XREAL_1:8;
A17: dist (y,y1) < ((dist (x,y)) - (diameter S)) / 2 by A11, METRIC_1:11;
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:8;
hence contradiction by METRIC_1:4; :: thesis: verum

end;

A18: now :: thesis: for x, y being Point of M st x in CL & y in CL holds
dist (x,y) <= (diameter S) + 1

A19: (diameter S) + 0 < (diameter S) + 1 by XREAL_1:8;
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 :: thesis: for s being Real st ( for x, y being Point of M st x in CL & y in CL holds
dist (x,y) <= s ) holds
diameter S <= s

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 :: thesis: for x, y being Point of M st x in S & y in S holds
dist (x,y) <= s

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:18;
hence dist (x,y) <= s by A23, A24, A25; :: thesis: verum

end;

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

end;

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