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