:: deftheorem defines Sphere CLVECT_2:def 7 :
for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds Sphere (x,r) = { y where y is Point of X : ||.(x - y).|| = r } ;