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 number 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 number st A c= Ball a,r
let a be Point of (TOP-REAL n); :: thesis: ex r being positive real number st A c= Ball a,r
reconsider C = A as bounded Subset of (Euclid n) by JORDAN2C:def 2;
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 10;
reconsider r = r as positive real number by A1;
reconsider x1 = x as Point of (TOP-REAL n) by TOPREAL3:13;
take s = r + |.(x1 - a).|; :: thesis: A c= Ball a,s
let p be set ; :: 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:13;
A4: dist p,x < r by A2, A3, METRIC_1:12;
A5: |.(p1 - x1).| = dist p,x by SPPOL_1:62;
A6: |.(p1 - a).| <= |.(p1 - x1).| + |.(x1 - a).| by TOPRNS_1:35;
|.(p1 - x1).| + |.(x1 - a).| < s by A4, A5, XREAL_1:8;
then |.(p1 - a).| < s by A6, XXREAL_0:2;
hence p in Ball a,s by TOPREAL9:7; :: thesis: verum