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

hence low_toler f,a is_symmetric_in X by RELAT_2:def 3; :: thesis: verum