let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL
for a being Real st low_toler (f,a) is_reflexive_in X & f is symmetric holds
(low_toler (f,a)) [*] is Equivalence_Relation of X
let f be PartFunc of [:X,X:],REAL; :: thesis: for a being Real st low_toler (f,a) is_reflexive_in X & f is symmetric holds
(low_toler (f,a)) [*] is Equivalence_Relation of X
let a be Real; :: thesis: ( low_toler (f,a) is_reflexive_in X & f is symmetric implies (low_toler (f,a)) [*] is Equivalence_Relation of X )
assume that
A1: low_toler (f,a) is_reflexive_in X and
A2: f is symmetric ; :: thesis: (low_toler (f,a)) [*] is Equivalence_Relation of X
dom (low_toler (f,a)) = X by A1, Th3;
then AA: X c= field (low_toler (f,a)) by XBOOLE_1:7;

now :: thesis: for x, y being object st x in X & y in X & [x,y] in low_toler (f,a) holds
[y,x] in low_toler (f,a)

let x, y be object ; :: thesis: ( x in X & y in X & [x,y] in low_toler (f,a) implies [y,x] in low_toler (f,a) )
assume that
A3: ( x in X & y in X ) and
A4: [x,y] in low_toler (f,a) ; :: thesis: [y,x] in low_toler (f,a)
reconsider x1 = x, y1 = y as Element of X by A3;
f . (x1,y1) <= a by A4, Def3;
then f . (y1,x1) <= a by A2, METRIC_1:def 4;
hence [y,x] in low_toler (f,a) by Def3; :: thesis: verum

end;

then low_toler (f,a) is_symmetric_in X by RELAT_2:def 3;
hence (low_toler (f,a)) [*] is Equivalence_Relation of X by AA, Th9; :: thesis: verum