let M be non empty MetrSpace; :: thesis: for A being non empty Subset of M
for B being Subset of M
for B' being Subset of (M | A) st B = B' & B is bounded holds
diameter B' <= diameter B
let A be non empty Subset of M; :: thesis: for B being Subset of M
for B' being Subset of (M | A) st B = B' & B is bounded holds
diameter B' <= diameter B
let B be Subset of M; :: thesis: for B' being Subset of (M | A) st B = B' & B is bounded holds
diameter B' <= diameter B
let B' be Subset of (M | A); :: thesis: ( B = B' & B is bounded implies diameter B' <= diameter B )
assume that
A1: B = B' and
A2: B is bounded ; :: thesis: diameter B' <= diameter B
A3: B' is bounded by A1, A2, Th15;

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

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

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

end;

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

now

let x, y be Point of (M | A); :: thesis: ( x in B' & y in B' implies dist x,y <= diameter B )
assume that
A6: x in B' and
A7: y in B' ; :: thesis: dist x,y <= diameter B
reconsider x' = x, y' = y as Point of M by TOPMETR:12;
dist x,y = dist x',y' by TOPMETR:def 1;
hence dist x,y <= diameter B by A1, A2, A6, A7, TBSP_1:def 10; :: thesis: verum

end;

hence diameter B' <= diameter B by A3, A5, TBSP_1:def 10; :: thesis: verum

end;

end;