for M being non empty MetrSpace
for x being Point of M holds (dist x) . x = 0