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_metr M implies z in fam_class the distance of M )
assume A1: z in fam_class_metr M ; :: thesis: z in fam_class the distance of M
consider a being non negative real number , R being Equivalence_Relation of M such that
A2: ( R = (dist_toler M,a) [*] & Class R = z ) by A1, Def8;
R = (low_toler the distance of M,a) [*] by A2, Th33;
hence z in fam_class the distance of M by A2, Def5; :: thesis: verum

end;

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

now

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

end;

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