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

let a be Real; :: thesis: dist_toler (M,a) = low_toler ( the distance of M,a)

hence dist_toler (M,a) = low_toler ( the distance of M,a) by A4, XBOOLE_0:def 10; :: thesis: verum

let a be Real; :: thesis: dist_toler (M,a) = low_toler ( the distance of M,a)

now :: thesis: for z being object st z in low_toler ( the distance of M,a) holds

z in dist_toler (M,a)

then A4:
low_toler ( the distance of M,a) c= dist_toler (M,a)
;z in dist_toler (M,a)

let z be object ; :: 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 object 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 ;

hence z in dist_toler (M,a) by A3, Def7; :: thesis: verum

end;assume A1: z in low_toler ( the distance of M,a) ; :: thesis: z in dist_toler (M,a)

consider x, y being object 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 ;

hence z in dist_toler (M,a) by A3, Def7; :: thesis: verum

now :: thesis: for z being object st z in dist_toler (M,a) holds

z in low_toler ( the distance of M,a)

then
dist_toler (M,a) c= low_toler ( the distance of M,a)
;z in low_toler ( the distance of M,a)

let z be object ; :: 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 object 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 ;

hence z in low_toler ( the distance of M,a) by A7, Def3; :: thesis: verum

end;assume A5: z in dist_toler (M,a) ; :: thesis: z in low_toler ( the distance of M,a)

consider x, y being object 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 ;

hence z in low_toler ( the distance of M,a) by A7, Def3; :: thesis: verum

hence dist_toler (M,a) = low_toler ( the distance of M,a) by A4, XBOOLE_0:def 10; :: thesis: verum