let r be real number ; :: thesis: for M being non empty MetrStruct
for p being Element of M holds cl_Ball p,r = { q where q is Element of M : dist p,q <= r }
let M be non empty MetrStruct ; :: thesis: for p being Element of M holds cl_Ball p,r = { q where q is Element of M : dist p,q <= r }
let p be Element of M; :: thesis: cl_Ball p,r = { q where q is Element of M : dist p,q <= r }
ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & cl_Ball p,r = { q where q is Element of M' : dist p',q <= r } ) by Def16;
hence cl_Ball p,r = { q where q is Element of M : dist p,q <= r } ; :: thesis: verum