let M be non empty Reflexive symmetric MetrStruct ; :: thesis: fam_class_metr M is Classification of the carrier of M

fam_class_metr M = fam_class the distance of M by Th35;

hence fam_class_metr M is Classification of the carrier of M by Th31; :: thesis: verum

fam_class_metr M = fam_class the distance of M by Th35;

hence fam_class_metr M is Classification of the carrier of M by Th31; :: thesis: verum