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 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

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 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