theorem :: CLVECT_2:56
for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)