theorem Th41: :: CLVECT_2:41

for X being ComplexUnitarySpace
for x, w being Point of X
for r being Real holds
( w in Ball (x,r) iff dist (x,w) < r )