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 holds
( B9 is bounded iff B is bounded )
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 holds
( B9 is bounded iff B is bounded )
let B be Subset of M; :: thesis: for B9 being Subset of (M | A) st B = B9 holds
( B9 is bounded iff B is bounded )
let B9 be Subset of (M | A); :: thesis: ( B = B9 implies ( B9 is bounded iff B is bounded ) )
assume A1: B = B9 ; :: thesis: ( B9 is bounded iff B is bounded )
thus ( B9 is bounded implies B is bounded ) by A1, HAUSDORF:19; :: thesis: ( B is bounded implies B9 is bounded )
assume A2: B is bounded ; :: thesis: B9 is bounded

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

suppose B9 = {} (M | A) ; :: thesis: B9 is bounded

hence B9 is bounded ; :: thesis: verum

end;

suppose B9 <> {} (M | A) ; :: thesis: B9 is bounded

then consider p being set such that
A3: p in B9 by XBOOLE_0:def 1;
reconsider p = p as Point of (M | A) by A3;

A4: now

let q be Point of (M | A); :: thesis: ( q in B9 implies dist p,q <= (diameter B) + 1 )
assume A5: q in B9 ; :: thesis: dist p,q <= (diameter B) + 1
reconsider p9 = p, q9 = q as Point of M by TOPMETR:12;
A6: dist p,q = dist p9,q9 by TOPMETR:def 1;
A7: (diameter B) + 0 <= (diameter B) + 1 by XREAL_1:10;
dist p9,q9 <= diameter B by A1, A2, A3, A5, TBSP_1:def 10;
hence dist p,q <= (diameter B) + 1 by A6, A7, XXREAL_0:2; :: thesis: verum

end;

0 + 0 < (diameter B) + 1 by A2, TBSP_1:29, XREAL_1:10;
hence B9 is bounded by A4, TBSP_1:15; :: thesis: verum

end;

end;