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

proof

assume A2: B' is bounded ; :: thesis: B is bounded
B' c= the carrier of (M | A) ;
then B' c= A by TOPMETR:def 2;
hence B is bounded by A1, A2, HAUSDORF:19; :: thesis: verum

end;

assume A3: B is bounded ; :: thesis: B' is bounded

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

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

hence B' is bounded ; :: thesis: verum

end;

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

then consider p being set such that
A4: p in B' by XBOOLE_0:def 1;
reconsider p = p as Point of (M | A) by A4;
A5: 0 + 0 < (diameter B) + 1 by A3, TBSP_1:29, XREAL_1:10;

now

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

end;

hence B' is bounded by A4, A5, TBSP_1:15; :: thesis: verum

end;

end;