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 9;
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 9; :: thesis: verum