let n be Element of NAT ; :: thesis: for p being Point of (Euclid n)
for q being Point of (TOP-REAL n)
for r being real number st p = q & r > 0 holds
Ball p,r is a_neighborhood of q
let p be Point of (Euclid n); :: thesis: for q being Point of (TOP-REAL n)
for r being real number st p = q & r > 0 holds
Ball p,r is a_neighborhood of q
let q be Point of (TOP-REAL n); :: thesis: for r being real number st p = q & r > 0 holds
Ball p,r is a_neighborhood of q
let r be real number ; :: thesis: ( p = q & r > 0 implies Ball p,r is a_neighborhood of q )
reconsider A = Ball p,r as Subset of (TOP-REAL n) by TOPREAL3:13;
assume ( p = q & r > 0 ) ; :: thesis: Ball p,r is a_neighborhood of q
then q in A by Th4;
hence Ball p,r is a_neighborhood of q by CONNSP_2:5, TOPMETR:21; :: thesis: verum