( the distance of M is nonnegative-yielding & the distance of M is symmetric ) by NonDist, METRIC_1:def 8;
hence SteinhausMetrSpace (M,p) is symmetric by METRIC_1:def 8; :: thesis: verum