theorem :: TOPREAL6:54

for M being non empty Reflexive discerning MetrStruct
for z being Point of M holds Sphere (z,0) = {z}