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

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