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