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 A1: ( B = B' & B is bounded ) ; :: thesis: diameter B' <= diameter B
A2: B' is bounded by A1, Th15;

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

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

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

end;

suppose A3: 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 A4: ( x in B' & 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, A4, TBSP_1:def 10; :: thesis: verum

end;

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

end;

end;