let X be non empty finite Subset of REAL ; :: thesis: for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being real number st z = rng f & A >= max z holds
(low_toler f,A) [*] = low_toler f,A
let f be Function of [:X,X:],REAL ; :: thesis: for z being non empty finite Subset of REAL
for A being real number st z = rng f & A >= max z holds
(low_toler f,A) [*] = low_toler f,A
let z be non empty finite Subset of REAL ; :: thesis: for A being real number st z = rng f & A >= max z holds
(low_toler f,A) [*] = low_toler f,A
let A be real number ; :: thesis: ( z = rng f & A >= max z implies (low_toler f,A) [*] = low_toler f,A )
assume A1: ( z = rng f & A >= max z ) ; :: thesis: (low_toler f,A) [*] = low_toler f,A

now

let p be set ; :: thesis: ( p in (low_toler f,A) [*] implies p in low_toler f,A )
assume p in (low_toler f,A) [*] ; :: thesis: p in low_toler f,A
then consider x, y being set such that
A2: ( x in X & y in X ) and
A3: p = [x,y] by ZFMISC_1:def 2;
reconsider x9 = x, y9 = y as Element of X by A2;
f . x9,y9 <= A by A1, Th26;
hence p in low_toler f,A by A3, Def3; :: thesis: verum

end;

then ( low_toler f,A c= (low_toler f,A) [*] & (low_toler f,A) [*] c= low_toler f,A ) by LANG1:18, TARSKI:def 3;
hence (low_toler f,A) [*] = low_toler f,A by XBOOLE_0:def 10; :: thesis: verum