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= B & 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= B & 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= B & A = C & C is bounded holds
A is bounded
let C be Subset of (M | B); :: thesis: ( A c= B & A = C & C is bounded implies A is bounded )
assume A1:
( A c= B & A = C & C is bounded )
; :: thesis: A is bounded
then consider r0 being Real such that
A2:
( 0 < r0 & ( for x, y being Point of (M | B) st x in C & y in C holds
dist x,y <= r0 ) )
by 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 A3:
(
x in A &
y in A )
;
:: thesis: dist x,y <= r0
then reconsider x0 =
x,
y0 =
y as
Point of
(M | B) by A1;
A4:
dist x0,
y0 <= r0
by A1, A2, A3;
A5:
the
distance of
(M | B) . x0,
y0 = the
distance of
M . x,
y
by TOPMETR:def 1;
the
distance of
(M | B) . x0,
y0 = dist x0,
y0
by METRIC_1:def 1;
hence
dist x,
y <= r0
by A4, A5, METRIC_1:def 1;
:: thesis: verum
end;
hence
A is bounded
by A2, TBSP_1:def 9; :: thesis: verum