let n be Element of NAT ; 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); 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); 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).|; A c= Ball (a,s)
let p be object ; TARSKI:def 3 ( not p in A or p in Ball (a,s) )
assume A3:
p in A
; 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; verum