for r being Real
for M being MetrStruct
for p, x being Element of M holds
( x in Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) )