theorem Th16: :: TAXONOM1:16

for X being non empty set
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