let X be non empty set ; 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; 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; ( 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 )
; 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 ;
( x in X & x = y implies [x,y] in (low_toler (f,0)) [*] )
assume
(
x in X &
x = y )
;
[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;
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 ;
( [x,y] in (low_toler (f,0)) [*] implies ( x in X & x = y ) )
assume
[x,y] in (low_toler (f,0)) [*]
;
( 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;
verum
end;
hence
R = id X
by A1, A3, RELAT_1:def 10; verum