let M be non empty MetrSpace; :: thesis: for A being non empty Subset of
for B being Subset of
for B' being Subset of st B = B' holds
( B' is bounded iff B is bounded )
let A be non empty Subset of ; :: thesis: for B being Subset of
for B' being Subset of st B = B' holds
( B' is bounded iff B is bounded )
let B be Subset of ; :: thesis: for B' being Subset of st B = B' holds
( B' is bounded iff B is bounded )
let B' be Subset of ; :: 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 ) by A1, HAUSDORF:19; :: thesis: ( B is bounded implies B' is bounded )
assume A2: 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
A3: p in B' by XBOOLE_0:def 1;
reconsider p = p as Point of by A3;

A4: now

let q be Point of ; :: thesis: ( q in B' implies dist p,q <= (diameter B) + 1 )
assume A5: q in B' ; :: thesis: dist p,q <= (diameter B) + 1
reconsider p' = p, q' = q as Point of by TOPMETR:12;
A6: dist p,q = dist p',q' by TOPMETR:def 1;
A7: (diameter B) + 0 <= (diameter B) + 1 by XREAL_1:10;
dist p',q' <= 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 B' is bounded by A4, TBSP_1:15; :: thesis: verum

end;

end;