let M be non empty Reflexive symmetric triangle MetrStruct ; 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; ( 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
; 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); ( S = S9 & CL = Cl S9 implies ( CL is bounded & diameter S = diameter CL ) )
assume that
A2:
S = S9
and
A3:
CL = Cl S9
; ( CL is bounded & diameter S = diameter CL )
per cases
( S <> {} or S = {} )
;
suppose A4:
S <> {}
;
( CL is bounded & diameter S = diameter CL )A5:
now for x, y being Point of M st x in CL & y in CL holds
not dist (x,y) > diameter Slet x,
y be
Point of
M;
( x in CL & y in CL implies not dist (x,y) > diameter S )assume that A6:
x in CL
and A7:
y in CL
;
not dist (x,y) > diameter Sreconsider 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
;
contradictionthen
(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;
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;
verum end; end;