for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a1, a2 being Real st a1 <= a2 holds
low_toler (f,a1) c= low_toler (f,a2)