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 M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & cl_Ball (p,r) = { q where q is Element of M9 : dist (p9,q) <= r } ) by Def16;
hence cl_Ball (p,r) = { q where q is Element of M : dist (p,q) <= r } ; :: thesis: verum