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

now :: thesis: for x being object st x in X holds
[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;

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