let M be non empty MetrStruct ; :: thesis: for a being real number holds dist_toler M,a = low_toler the distance of M,a
let a be real number ; :: thesis: dist_toler M,a = low_toler the distance of M,a

now

let z be set ; :: thesis: ( z in low_toler the distance of M,a implies z in dist_toler M,a )
assume A1: z in low_toler the distance of M,a ; :: thesis: z in dist_toler M,a
consider x, y being set such that
A2: ( x in the carrier of M & y in the carrier of M ) and
A3: z = [x,y] by A1, ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Element of M by A2;
dist x1,y1 = the distance of M . x1,y1 by METRIC_1:def 1;
then dist x1,y1 <= a by A1, A3, Def3;
then x1,y1 are_in_tolerance_wrt a by Def6;
hence z in dist_toler M,a by A3, Def7; :: thesis: verum

end;

then A4: low_toler the distance of M,a c= dist_toler M,a by TARSKI:def 3;

now

let z be set ; :: thesis: ( z in dist_toler M,a implies z in low_toler the distance of M,a )
assume A5: z in dist_toler M,a ; :: thesis: z in low_toler the distance of M,a
consider x, y being set such that
A6: ( x in the carrier of M & y in the carrier of M ) and
A7: z = [x,y] by A5, ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Element of M by A6;
( the distance of M . x1,y1 = dist x1,y1 & x1,y1 are_in_tolerance_wrt a ) by A5, A7, Def7, METRIC_1:def 1;
then the distance of M . x1,y1 <= a by Def6;
hence z in low_toler the distance of M,a by A7, Def3; :: thesis: verum

end;

then dist_toler M,a c= low_toler the distance of M,a by TARSKI:def 3;
hence dist_toler M,a = low_toler the distance of M,a by A4, XBOOLE_0:def 10; :: thesis: verum