let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL
for x, y being set 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 set st f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler f,0 holds
x = y
let x, y be set ; :: 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:106;
f . x1,y1 <= 0 by A2, Def3;
then f . x1,y1 = 0 by A1, Def4;
hence x = y by A1, METRIC_1:def 4; :: thesis: verum