let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL st f is nonnegative & f is Reflexive & f is discerning holds
(low_toler f,0 ) [*] = low_toler f,0
let f be PartFunc of [:X,X:],REAL ; :: thesis: ( f is nonnegative & f is Reflexive & f is discerning implies (low_toler f,0 ) [*] = low_toler f,0 )
assume A1: ( f is nonnegative & f is Reflexive & f is discerning ) ; :: thesis: (low_toler f,0 ) [*] = low_toler f,0
A2: low_toler f,0 c= (low_toler f,0 ) [*] by LANG1:18;

now

let p be set ; :: thesis: ( p in (low_toler f,0 ) [*] implies p in low_toler f,0 )
assume A3: p in (low_toler f,0 ) [*] ; :: thesis: p in low_toler f,0
consider x, y being set such that
A4: p = [x,y] by A3, RELAT_1:def 1;
low_toler f,0 reduces x,y by A3, A4, REWRITE1:21;
then consider r being RedSequence of low_toler f,0 such that
A5: ( r . 1 = x & r . (len r) = y ) by REWRITE1:def 3;
0 < len r by REWRITE1:def 2;
then 0 + 1 <= len r by NAT_1:13;
then A6: ( 1 in dom r & len r in dom r ) by FINSEQ_3:27;

now

let i be Nat; :: thesis: ( i in dom r & i + 1 in dom r implies r . i = r . (i + 1) )
assume A7: ( i in dom r & i + 1 in dom r ) ; :: thesis: r . i = r . (i + 1)
[(r . i),(r . (i + 1))] in low_toler f,0 by A7, REWRITE1:def 2;
hence r . i = r . (i + 1) by A1, Th20; :: thesis: verum

end;

then A8: r . 1 = r . (len r) by A6, Th2;
x is Element of X by A3, A4, ZFMISC_1:106;
hence p in low_toler f,0 by A1, A4, A5, A8, Th21; :: thesis: verum

end;

then (low_toler f,0 ) [*] c= low_toler f,0 by TARSKI:def 3;
hence (low_toler f,0 ) [*] = low_toler f,0 by A2, XBOOLE_0:def 10; :: thesis: verum