theorem Th51: :: BHSP_2:51

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