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

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