let M be non empty bounded MetrSpace; :: thesis: {the carrier of M} in fam_class_metr M
set a = diameter ([#] M);
the distance of M is symmetric by METRIC_1:def 9;
then low_toler the distance of M,(diameter ([#] M)) is_symmetric_in the carrier of M by Th17;
then A1: dist_toler M,(diameter ([#] M)) is_symmetric_in the carrier of M by Th33;
the distance of M is Reflexive by METRIC_1:def 7;
then low_toler the distance of M,(diameter ([#] M)) is_reflexive_in the carrier of M by Th16;
then dist_toler M,(diameter ([#] M)) is_reflexive_in the carrier of M by Th33;
then reconsider R = (dist_toler M,(diameter ([#] M))) [*] as Equivalence_Relation of M by A1, Th9;
Class R = {the carrier of M} by Th40;
hence {the carrier of M} in fam_class_metr M by Def8; :: thesis: verum