theorem :: METRIC_1:16

for r being Real
for M being MetrStruct
for p being Element of M holds (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r)