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