let M be non empty MetrSpace; for A being non empty Subset of M
for B being Subset of M
for B9 being Subset of (M | A) st B = B9 holds
( B9 is bounded iff B is bounded )
let A be non empty Subset of M; for B being Subset of M
for B9 being Subset of (M | A) st B = B9 holds
( B9 is bounded iff B is bounded )
let B be Subset of M; for B9 being Subset of (M | A) st B = B9 holds
( B9 is bounded iff B is bounded )
let B9 be Subset of (M | A); ( B = B9 implies ( B9 is bounded iff B is bounded ) )
assume A1:
B = B9
; ( B9 is bounded iff B is bounded )
thus
( B9 is bounded implies B is bounded )
by A1, HAUSDORF:17; ( B is bounded implies B9 is bounded )
assume A2:
B is bounded
; B9 is bounded
per cases
( B9 = {} (M | A) or B9 <> {} (M | A) )
;
suppose
B9 <> {} (M | A)
;
B9 is bounded then consider p being
object such that A3:
p in B9
by XBOOLE_0:def 1;
reconsider p =
p as
Point of
(M | A) by A3;
A4:
now for q being Point of (M | A) st q in B9 holds
dist (p,q) <= (diameter B) + 1let q be
Point of
(M | A);
( q in B9 implies dist (p,q) <= (diameter B) + 1 )assume A5:
q in B9
;
dist (p,q) <= (diameter B) + 1reconsider p9 =
p,
q9 =
q as
Point of
M by TOPMETR:8;
A6:
dist (
p,
q)
= dist (
p9,
q9)
by TOPMETR:def 1;
A7:
(diameter B) + 0 <= (diameter B) + 1
by XREAL_1:8;
dist (
p9,
q9)
<= diameter B
by A1, A2, A3, A5, TBSP_1:def 8;
hence
dist (
p,
q)
<= (diameter B) + 1
by A6, A7, XXREAL_0:2;
verum end;
0 + 0 < (diameter B) + 1
by A2, TBSP_1:21, XREAL_1:8;
hence
B9 is
bounded
by A4, TBSP_1:10;
verum end; end;