let n be Element of NAT ; :: thesis: for A being closed Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st not p in A holds
ex r being positive Real st Ball (p,r) misses A
let A be closed Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n) st not p in A holds
ex r being positive Real st Ball (p,r) misses A
let p be Point of (TOP-REAL n); :: thesis: ( not p in A implies ex r being positive Real st Ball (p,r) misses A )
assume not p in A ; :: thesis: ex r being positive Real st Ball (p,r) misses A
then A1: p in A ` by SUBSET_1:29;
reconsider e = p as Point of (Euclid n) by TOPREAL3:8;
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider AA = A ` as Subset of (TopSpaceMetr (Euclid n)) ;
AA is open by A2, PRE_TOPC:30;
then consider r being Real such that
A3: r > 0 and
A4: Ball (e,r) c= A ` by A1, TOPMETR:15;
reconsider r = r as positive Real by A3;
take r ; :: thesis: Ball (p,r) misses A
Ball (p,r) = Ball (e,r) by TOPREAL9:13;
hence Ball (p,r) misses A by A4, SUBSET_1:23; :: thesis: verum