let M be non empty MetrSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( B = B9 & B is bounded implies diameter B9 <= diameter B )
assume that
A1: B = B9 and
A2: B is bounded ; :: thesis: diameter B9 <= diameter B
A3: B9 is bounded by A1, A2, Th15;

per cases ( B9 = {} (M | A) or B9 <> {} (M | A) ) ;

suppose A4: B9 = {} (M | A) ; :: thesis: diameter B9 <= diameter B

then diameter B9 = 0 by TBSP_1:def 8;
hence diameter B9 <= diameter B by A1, A4, TBSP_1:def 8; :: thesis: verum

end;

suppose A5: B9 <> {} (M | A) ; :: thesis: diameter B9 <= diameter B

now :: thesis: for x, y being Point of (M | A) st x in B9 & y in B9 holds
dist (x,y) <= diameter B

let x, y be Point of (M | A); :: thesis: ( x in B9 & y in B9 implies dist (x,y) <= diameter B )
assume that
A6: x in B9 and
A7: y in B9 ; :: thesis: dist (x,y) <= diameter B
reconsider 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; :: thesis: verum

end;

hence diameter B9 <= diameter B by A3, A5, TBSP_1:def 8; :: thesis: verum

end;

end;