let n be Nat; :: thesis:
let A be Subset of (TOP-REAL n); :: thesis:
let p be Point of (TOP-REAL n); :: thesis:
let p9 be Point of (Euclid n); :: thesis:
assume A1: p = p9 ; :: thesis:
let s be Real; :: thesis:
assume A2: s > 0 ; :: thesis:

hereby :: thesis:

assume A3: p in Cl A ; :: thesis:
let r be Real; :: thesis:
assume that
A4: 0 < r and
r < s ; :: thesis:
reconsider B = Ball (p9,r) as Subset of (TOP-REAL n) by TOPREAL3:8;
B is a_neighborhood of p by A1, A4, Th2;
hence Ball (p9,r) meets A by A3, CONNSP_2:27; :: thesis:

end;

assume A5: for r being Real st 0 < r & r < s holds
Ball (p9,r) meets A ; :: thesis:
for G being a_neighborhood of p holds G meets A

let G be a_neighborhood of p; :: thesis:
p in Int G by CONNSP_2:def 1;
then consider r9 being Real such that
A6: r9 > 0 and
A7: Ball (p9,r9) c= G by A1, Th5;
set r = min (r9,(s / 2));
Ball (p9,(min (r9,(s / 2)))) c= Ball (p9,r9) by PCOMPS_1:1, XXREAL_0:17;
then A8: Ball (p9,(min (r9,(s / 2)))) c= G by A7;
( s / 2 < s & min (r9,(s / 2)) <= s / 2 ) by A2, XREAL_1:216, XXREAL_0:17;
then A9: min (r9,(s / 2)) < s by XXREAL_0:2;
s / 2 > 0 by A2, XREAL_1:215;
then min (r9,(s / 2)) > 0 by A6, XXREAL_0:15;
hence G meets A by A5, A8, A9, XBOOLE_1:63; :: thesis:

end;

hence p in Cl A by CONNSP_2:27; :: thesis: