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 dist_toler M,a implies z in low_toler the distance of M,a )assume A1:
z in dist_toler M,
a
;
:: thesis: z in low_toler the distance of M,aconsider x,
y being
set such that A2:
(
x in the
carrier of
M &
y in the
carrier of
M &
z = [x,y] )
by A1, ZFMISC_1:def 2;
reconsider x1 =
x,
y1 =
y as
Element of
M by A2;
A3:
the
distance of
M . x1,
y1 = dist x1,
y1
by METRIC_1:def 1;
x1,
y1 are_in_tolerance_wrt a
by A1, A2, Def7;
then
the
distance of
M . x1,
y1 <= a
by A3, Def6;
hence
z in low_toler the
distance of
M,
a
by A2, Def3;
:: thesis: verum end;
then A4:
dist_toler M,a c= low_toler the distance of M,a
by TARSKI:def 3;
now let z be
set ;
:: thesis: ( z in low_toler the distance of M,a implies z in dist_toler M,a )assume A5:
z in low_toler the
distance of
M,
a
;
:: thesis: z in dist_toler M,aconsider x,
y being
set such that A6:
(
x in the
carrier of
M &
y in the
carrier of
M &
z = [x,y] )
by A5, ZFMISC_1:def 2;
reconsider x1 =
x,
y1 =
y as
Element of
M by A6;
dist x1,
y1 = the
distance of
M . x1,
y1
by METRIC_1:def 1;
then
dist x1,
y1 <= a
by A5, A6, Def3;
then
x1,
y1 are_in_tolerance_wrt a
by Def6;
hence
z in dist_toler M,
a
by A6, Def7;
:: thesis: verum end;
then
low_toler the distance of M,a c= dist_toler 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