let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL
for a being real number 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 number 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 number ; :: thesis: ( low_toler f,a is_reflexive_in X & f is symmetric implies (low_toler f,a) [*] is Equivalence_Relation of X )
assume A1: ( low_toler f,a is_reflexive_in X & f is symmetric ) ; :: thesis: (low_toler f,a) [*] is Equivalence_Relation of X

now

let x, y be set ; :: thesis: ( x in X & y in X & [x,y] in low_toler f,a implies [y,x] in low_toler f,a )
assume A2: ( x in X & y in X & [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 A2;
f . x1,y1 <= a by A2, Def3;
then f . y1,x1 <= a by A1, METRIC_1:def 5;
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 A1, Th9; :: thesis: verum