let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL

for a being Real 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 st f is symmetric holds

low_toler (f,a) is_symmetric_in X

let a be Real; :: 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

for a being Real 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 st f is symmetric holds

low_toler (f,a) is_symmetric_in X

let a be Real; :: 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 :: 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)

hence
low_toler (f,a) is_symmetric_in X
by RELAT_2:def 3; :: thesis: verum[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

A2: ( x in X & y in X ) and

A3: [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 A3, Def3;

then f . (y1,x1) <= a by A1, METRIC_1:def 4;

hence [y,x] in low_toler (f,a) by Def3; :: thesis: verum

end;assume that

A2: ( x in X & y in X ) and

A3: [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 A3, Def3;

then f . (y1,x1) <= a by A1, METRIC_1:def 4;

hence [y,x] in low_toler (f,a) by Def3; :: thesis: verum