let n be Element of NAT ; :: thesis: for A being bounded Subset of (TOP-REAL n)
for a being Point of (TOP-REAL n) ex r being positive Real st A c= Ball (a,r)
let A be bounded Subset of (TOP-REAL n); :: thesis: for a being Point of (TOP-REAL n) ex r being positive Real st A c= Ball (a,r)
let a be Point of (TOP-REAL n); :: thesis: ex r being positive Real st A c= Ball (a,r)
reconsider C = A as bounded Subset of (Euclid n) by JORDAN2C:11;
consider r being Real, x being Element of (Euclid n) such that
A1: 0 < r and
A2: C c= Ball (x,r) by METRIC_6:def 3;
reconsider r = r as positive Real by A1;
reconsider x1 = x as Point of (TOP-REAL n) by TOPREAL3:8;
take s = r + |.(x1 - a).|; :: thesis: A c= Ball (a,s)
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in A or p in Ball (a,s) )
assume A3: p in A ; :: thesis: p in Ball (a,s)
then reconsider p1 = p as Point of (TOP-REAL n) ;
p = p1 ;
then reconsider p = p as Point of (Euclid n) by TOPREAL3:8;
A4: dist (p,x) < r by A2, A3, METRIC_1:11;
A5: |.(p1 - x1).| = dist (p,x) by SPPOL_1:39;
A6: |.(p1 - a).| <= |.(p1 - x1).| + |.(x1 - a).| by TOPRNS_1:34;
|.(p1 - x1).| + |.(x1 - a).| < s by A4, A5, XREAL_1:6;
then |.(p1 - a).| < s by A6, XXREAL_0:2;
hence p in Ball (a,s) by TOPREAL9:7; :: thesis: verum