let X be non empty set ; :: thesis: 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)
let f be PartFunc of [:X,X:],REAL; :: thesis: for a1, a2 being Real st a1 <= a2 holds
low_toler (f,a1) c= low_toler (f,a2)
let a1, a2 be Real; :: 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)
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in low_toler (f,a1) or 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 object 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: verum