let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL
for R being Equivalence_Relation of X st R = (low_toler f,0 ) [*] & f is nonnegative & f is Reflexive & f is discerning holds
R = id X
let f be PartFunc of [:X,X:],REAL ; :: thesis: for R being Equivalence_Relation of X st R = (low_toler f,0 ) [*] & f is nonnegative & f is Reflexive & f is discerning holds
R = id X
let R be Equivalence_Relation of X; :: thesis: ( R = (low_toler f,0 ) [*] & f is nonnegative & f is Reflexive & f is discerning implies R = id X )
assume A1: ( R = (low_toler f,0 ) [*] & f is nonnegative & f is Reflexive & f is discerning ) ; :: thesis: R = id X
A2: for x, y being set st [x,y] in (low_toler f,0 ) [*] holds
( x in X & x = y )

proof

let x, y be set ; :: thesis: ( [x,y] in (low_toler f,0 ) [*] implies ( x in X & x = y ) )
assume [x,y] in (low_toler f,0 ) [*] ; :: thesis: ( x in X & x = y )
then [x,y] in low_toler f,0 by A1, Th23;
hence ( x in X & x = y ) by A1, Th20, ZFMISC_1:106; :: thesis: verum

end;

for x, y being set st x in X & x = y holds
[x,y] in (low_toler f,0 ) [*]

proof

let x, y be set ; :: thesis: ( x in X & x = y implies [x,y] in (low_toler f,0 ) [*] )
assume ( x in X & x = y ) ; :: thesis: [x,y] in (low_toler f,0 ) [*]
then [x,y] in low_toler f,0 by A1, Th21;
hence [x,y] in (low_toler f,0 ) [*] by A1, Th23; :: thesis: verum

end;

hence R = id X by A1, A2, RELAT_1:def 10; :: thesis: verum