let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL
for x, y being object st f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) holds
x = y
let f be PartFunc of [:X,X:],REAL; :: thesis: for x, y being object st f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) holds
x = y
let x, y be object ; :: thesis: ( f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) implies x = y )
assume A1: ( f is nonnegative & f is Reflexive & f is discerning ) ; :: thesis: ( not [x,y] in low_toler (f,0) or x = y )
assume A2: [x,y] in low_toler (f,0) ; :: thesis: x = y
then reconsider x1 = x, y1 = y as Element of X by ZFMISC_1:87;
f . (x1,y1) <= 0 by A2, Def3;
then f . (x1,y1) = 0 by A1;
hence x = y by A1, METRIC_1:def 3; :: thesis: verum