theorem Th51: :: CLVECT_2:51

for X being ComplexUnitarySpace
for x, w being Point of X
for r being Real holds
( w in Sphere (x,r) iff ||.(x - w).|| = r )