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 A2, Th21;
hence [x,y] in (low_toler (f,0)) [*] by A2, Th23; :: 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 A2, Th23;
hence ( x in X & x = y ) by A2, Th20, ZFMISC_1:87; :: thesis: verum
end;
hence R = id X by A1, A3, RELAT_1:def 10; :: thesis: verum