let M be non empty MetrSpace; :: thesis: for A being Subset of M
for B being non empty Subset of M
for C being Subset of (M | B) st A = C & C is bounded holds
A is bounded
let A be Subset of M; :: thesis: for B being non empty Subset of M
for C being Subset of (M | B) st A = C & C is bounded holds
A is bounded
let B be non empty Subset of M; :: thesis: for C being Subset of (M | B) st A = C & C is bounded holds
A is bounded
let C be Subset of (M | B); :: thesis: ( A = C & C is bounded implies A is bounded )
assume that
A1: A = C and
A2: C is bounded ; :: thesis: A is bounded
consider r0 being Real such that
A3: 0 < r0 and
A4: for x, y being Point of (M | B) st x in C & y in C holds
dist (x,y) <= r0 by A2, TBSP_1:def 7;
for x, y being Point of M st x in A & y in A holds
dist (x,y) <= r0

proof

let x, y be Point of M; :: thesis: ( x in A & y in A implies dist (x,y) <= r0 )
assume A5: ( x in A & y in A ) ; :: thesis: dist (x,y) <= r0
then reconsider x0 = x, y0 = y as Point of (M | B) by A1;
A6: ( the distance of (M | B) . (x0,y0) = the distance of M . (x,y) & the distance of (M | B) . (x0,y0) = dist (x0,y0) ) by METRIC_1:def 1, TOPMETR:def 1;
dist (x0,y0) <= r0 by A1, A4, A5;
hence dist (x,y) <= r0 by A6, METRIC_1:def 1; :: thesis: verum

end;

hence A is bounded by A3, TBSP_1:def 7; :: thesis: verum