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