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 number 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 number 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 number st Ball p,r misses A )
assume not p in A ; :: thesis: ex r being positive real number st Ball p,r misses A
then A1: p in A ` by SUBSET_1:50;
reconsider e = p as Point of (Euclid n) by TOPREAL3:13;
consider r being real number such that
A2: r > 0 and
A3: Ball e,r c= A ` by A1, TOPMETR:22;
reconsider r = r as positive real number by A2;
take r ; :: thesis: Ball p,r misses A
Ball p,r = Ball e,r by TOPREAL9:13;
hence Ball p,r misses A by A3, SUBSET_1:43; :: thesis: verum