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

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

now :: thesis: for z being object st z in fam_class the distance of M holds

z in fam_class_metr M

then A3:
fam_class the distance of M c= fam_class_metr M
;z in fam_class_metr M

let z be object ; :: 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, 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;assume z in fam_class the distance of M ; :: thesis: z in fam_class_metr M

then consider a being non negative Real, 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

now :: thesis: for z being object st z in fam_class_metr M holds

z in fam_class the distance of M

then
fam_class_metr M c= fam_class the distance of M
;z in fam_class the distance of M

let z be object ; :: 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, 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;assume z in fam_class_metr M ; :: thesis: z in fam_class the distance of M

then consider a being non negative Real, 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

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