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 8;
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 6;
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 dom (dist_toler (M,(diameter ([#] M)))) = the carrier of M by Th3;
then the carrier of M c= field (dist_toler (M,(diameter ([#] M)))) by XBOOLE_1:7;
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