let X be non empty set ; 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; 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 ; ( 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 )
; ( not [x,y] in low_toler (f,0) or x = y )
assume A2:
[x,y] in low_toler (f,0)
; 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; verum