reconsider a = 0 as non negative real number ;
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 9;
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 7;
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