let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL
for a being real number 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 number st f is Reflexive & a >= 0 holds
low_toler f,a is_reflexive_in X
let a be real number ; :: 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

let x be set ; :: thesis: ( x in X implies [x,x] in low_toler f,a )
assume A2: x in X ; :: thesis: [x,x] in low_toler f,a
reconsider x1 = x as Element of X by A2;
f . x1,x1 <= a by A1, METRIC_1:def 3;
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