let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL
for x being Element of X st f is Reflexive & f is discerning holds
[x,x] in low_toler (f,0)
let f be PartFunc of [:X,X:],REAL; :: thesis: for x being Element of X st f is Reflexive & f is discerning holds
[x,x] in low_toler (f,0)
let x be Element of X; :: thesis: ( f is Reflexive & f is discerning implies [x,x] in low_toler (f,0) )
assume ( f is Reflexive & f is discerning ) ; :: thesis: [x,x] in low_toler (f,0)
then f . (x,x) = 0 by METRIC_1:def 2;
hence [x,x] in low_toler (f,0) by Def3; :: thesis: verum