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

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