reconsider a = 0 as non negative Real ;
let M be non empty bounded MetrSpace; :: thesis: fam_class_metr M is Strong_Classification of the carrier of M
the distance of M is symmetric by METRIC_1:def 8;
then low_toler ( the distance of M,a) is_symmetric_in the carrier of M by Th17;
then A1: dist_toler (M,a) 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,a) is_reflexive_in the carrier of M by Th16;
then dist_toler (M,a) is_reflexive_in the carrier of M by Th33;
then reconsider R = (dist_toler (M,a)) [*] as Equivalence_Relation of M by A1, Th9;
Class R in fam_class_metr M by Def8;
then A2: SmallestPartition the carrier of M in fam_class_metr M by Th36;
( fam_class_metr M is Classification of the carrier of M & { the carrier of M} in fam_class_metr M ) by Th41, Th42;
hence fam_class_metr M is Strong_Classification of the carrier of M by A2, Def2; :: thesis: verum