the distance of M is nonnegative-yielding by NonDist;
hence SteinhausMetrSpace (M,p) is with_nonnegative_distance ; :: thesis: verum