let M be non empty MetrSpace; :: thesis: for p being Point of
for q being Point of
for r being real number st p = q & r > 0 holds
Ball p,r is a_neighborhood of q
let p be Point of ; :: thesis: for q being Point of
for r being real number st p = q & r > 0 holds
Ball p,r is a_neighborhood of q
let q be Point of ; :: 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 by TOPMETR:16;
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