let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL
for a1, a2 being real number st a1 <= a2 holds
low_toler f,a1 c= low_toler f,a2
let f be PartFunc of [:X,X:],REAL ; :: thesis: for a1, a2 being real number st a1 <= a2 holds
low_toler f,a1 c= low_toler f,a2
let a1, a2 be real number ; :: thesis: ( a1 <= a2 implies low_toler f,a1 c= low_toler f,a2 )
assume A1: a1 <= a2 ; :: thesis: low_toler f,a1 c= low_toler f,a2

now

let p be set ; :: thesis: ( p in low_toler f,a1 implies p in low_toler f,a2 )
assume A2: p in low_toler f,a1 ; :: thesis: p in low_toler f,a2
consider x, y being set such that
A3: ( x in X & y in X & 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, A3, Def3;
then f . x1,y1 <= a2 by A1, XXREAL_0:2;
hence p in low_toler f,a2 by A3, Def3; :: thesis: verum

end;

hence low_toler f,a1 c= low_toler f,a2 by TARSKI:def 3; :: thesis: verum