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

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