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