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