let M be non empty MetrSpace; for A being non empty Subset of M
for B being Subset of M
for B9 being Subset of (M | A) st B = B9 & B is bounded holds
diameter B9 <= diameter B
let A be non empty Subset of M; for B being Subset of M
for B9 being Subset of (M | A) st B = B9 & B is bounded holds
diameter B9 <= diameter B
let B be Subset of M; for B9 being Subset of (M | A) st B = B9 & B is bounded holds
diameter B9 <= diameter B
let B9 be Subset of (M | A); ( B = B9 & B is bounded implies diameter B9 <= diameter B )
assume that
A1:
B = B9
and
A2:
B is bounded
; diameter B9 <= diameter B
A3:
B9 is bounded
by A1, A2, Th15;
per cases
( B9 = {} (M | A) or B9 <> {} (M | A) )
;
suppose A5:
B9 <> {} (M | A)
;
diameter B9 <= diameter Bnow for x, y being Point of (M | A) st x in B9 & y in B9 holds
dist (x,y) <= diameter Blet x,
y be
Point of
(M | A);
( x in B9 & y in B9 implies dist (x,y) <= diameter B )assume that A6:
x in B9
and A7:
y in B9
;
dist (x,y) <= diameter Breconsider x9 =
x,
y9 =
y as
Point of
M by TOPMETR:8;
dist (
x,
y)
= dist (
x9,
y9)
by TOPMETR:def 1;
hence
dist (
x,
y)
<= diameter B
by A1, A2, A6, A7, TBSP_1:def 8;
verum end; hence
diameter B9 <= diameter B
by A3, A5, TBSP_1:def 8;
verum end; end;