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

for a being Real st f is Reflexive & a >= 0 holds

low_toler (f,a) is_reflexive_in X

let f be PartFunc of [:X,X:],REAL; :: thesis: for a being Real st f is Reflexive & a >= 0 holds

low_toler (f,a) is_reflexive_in X

let a be Real; :: thesis: ( f is Reflexive & a >= 0 implies low_toler (f,a) is_reflexive_in X )

assume A1: ( f is Reflexive & a >= 0 ) ; :: thesis: low_toler (f,a) is_reflexive_in X

for a being Real st f is Reflexive & a >= 0 holds

low_toler (f,a) is_reflexive_in X

let f be PartFunc of [:X,X:],REAL; :: thesis: for a being Real st f is Reflexive & a >= 0 holds

low_toler (f,a) is_reflexive_in X

let a be Real; :: thesis: ( f is Reflexive & a >= 0 implies low_toler (f,a) is_reflexive_in X )

assume A1: ( f is Reflexive & a >= 0 ) ; :: thesis: low_toler (f,a) is_reflexive_in X

now :: thesis: for x being object st x in X holds

[x,x] in low_toler (f,a)

hence
low_toler (f,a) is_reflexive_in X
by RELAT_2:def 1; :: thesis: verum[x,x] in low_toler (f,a)

let x be object ; :: thesis: ( x in X implies [x,x] in low_toler (f,a) )

assume x in X ; :: thesis: [x,x] in low_toler (f,a)

then reconsider x1 = x as Element of X ;

f . (x1,x1) <= a by A1, METRIC_1:def 2;

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

end;assume x in X ; :: thesis: [x,x] in low_toler (f,a)

then reconsider x1 = x as Element of X ;

f . (x1,x1) <= a by A1, METRIC_1:def 2;

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