let M be non empty Reflexive symmetric MetrStruct ; :: thesis: fam_class_metr M = fam_class the distance of M

now

let z be set ; :: thesis: ( z in fam_class the distance of M implies z in fam_class_metr M )
assume z in fam_class the distance of M ; :: thesis: z in fam_class_metr M
then consider a being non negative real number , R being Equivalence_Relation of the carrier of M such that
A1: R = (low_toler ( the distance of M,a)) [*] and
A2: Class R = z by Def5;
reconsider R1 = R as Equivalence_Relation of M ;
R1 = (dist_toler (M,a)) [*] by A1, Th33;
hence z in fam_class_metr M by A2, Def8; :: thesis: verum

end;

then A3: fam_class the distance of M c= fam_class_metr M by TARSKI:def 3;

now

let z be set ; :: thesis: ( z in fam_class_metr M implies z in fam_class the distance of M )
assume z in fam_class_metr M ; :: thesis: z in fam_class the distance of M
then consider a being non negative real number , R being Equivalence_Relation of M such that
A4: R = (dist_toler (M,a)) [*] and
A5: Class R = z by Def8;
R = (low_toler ( the distance of M,a)) [*] by A4, Th33;
hence z in fam_class the distance of M by A5, Def5; :: thesis: verum

end;

then fam_class_metr M c= fam_class the distance of M by TARSKI:def 3;
hence fam_class_metr M = fam_class the distance of M by A3, XBOOLE_0:def 10; :: thesis: verum