let M be non empty MetrStruct ; for a being Real holds dist_toler (M,a) = low_toler ( the distance of M,a)
let a be Real; dist_toler (M,a) = low_toler ( the distance of M,a)
now for z being object st z in low_toler ( the distance of M,a) holds
z in dist_toler (M,a)let z be
object ;
( 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)
;
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;
verum end;
then A4:
low_toler ( the distance of M,a) c= dist_toler (M,a)
;
now for z being object st z in dist_toler (M,a) holds
z in low_toler ( the distance of M,a)let z be
object ;
( z in dist_toler (M,a) implies z in low_toler ( the distance of M,a) )assume A5:
z in dist_toler (
M,
a)
;
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;
verum end;
then
dist_toler (M,a) c= 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; verum