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 3;
hence [x,x] in low_toler f,0 by Def3; :: thesis: verum