( the distance of M is V154() & the distance of M is discerning ) by NonDist, METRIC_1:def 7;
hence SteinhausMetrSpace (M,p) is discerning by METRIC_1:def 7; :: thesis: verum