let M be non empty MetrSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( B = B9 implies ( B9 is bounded iff B is bounded ) )
assume A1: B = B9 ; :: thesis: ( B9 is bounded iff B is bounded )
thus ( B9 is bounded implies B is bounded ) by A1, HAUSDORF:17; :: thesis: ( B is bounded implies B9 is bounded )
assume A2: B is bounded ; :: thesis: B9 is bounded
per cases ( B9 = {} (M | A) or B9 <> {} (M | A) ) ;
suppose B9 = {} (M | A) ; :: thesis: B9 is bounded
hence B9 is bounded ; :: thesis: verum
end;
suppose B9 <> {} (M | A) ; :: thesis: 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 :: thesis: for q being Point of (M | A) st q in B9 holds
dist (p,q) <= (diameter B) + 1
let q be Point of (M | A); :: thesis: ( q in B9 implies dist (p,q) <= (diameter B) + 1 )
assume A5: q in B9 ; :: thesis: dist (p,q) <= (diameter B) + 1
reconsider 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; :: thesis: verum
end;
0 + 0 < (diameter B) + 1 by A2, TBSP_1:21, XREAL_1:8;
hence B9 is bounded by A4, TBSP_1:10; :: thesis: verum
end;
end;