let X be non empty set ; :: thesis:
let f be PartFunc of [:X,X:],REAL; :: thesis:
let a1, a2 be real number ; :: thesis:
assume A1: a1 <= a2 ; :: thesis:

let p be set ; :: thesis:
assume A2: p in low_toler (f,a1) ; :: thesis:
consider x, y being set such that
A3: ( x in X & y in X ) and
A4: p = [x,y] by A2, ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Element of X by A3;
f . (x1,y1) <= a1 by A2, A4, Def3;
then f . (x1,y1) <= a2 by A1, XXREAL_0:2;
hence p in low_toler (f,a2) by A4, Def3; :: thesis:

end;