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)) [*]

( x in X & x = y )

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

for x, y being object st [x,y] in (low_toler (f,0)) [*] holds
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;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

( x in X & x = y )

proof

hence
R = id X
by A1, A3, RELAT_1:def 10; :: thesis: verum
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;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