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 that
A1: R = (low_toler (f,0)) [*] and
A2: ( f is nonnegative & f is Reflexive & f is discerning ) ; :: thesis: R = id X
A3: for x, y being object st x in X & x = y holds
[x,y] in (low_toler (f,0)) [*]
proof
let x, y be object ; :: 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 ;
hence [x,y] in (low_toler (f,0)) [*] by ; :: thesis: verum
end;
for x, y being object st [x,y] in (low_toler (f,0)) [*] holds
( x in X & x = y )
proof
let x, y be object ; :: 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 ;
hence ( x in X & x = y ) by ; :: thesis: verum
end;
hence R = id X by ; :: thesis: verum