theorem :: TAXONOM1:43

for M being non empty bounded MetrSpace holds fam_class_metr M is Strong_Classification of the carrier of M