:: deftheorem Def3 defines low_toler TAXONOM1:def 3 :
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being Real
for b₄ being Relation of X holds
( b₄ = low_toler (f,a) iff for x, y being Element of X holds
( [x,y] in b₄ iff f . (x,y) <= a ) );