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 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 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 st z = rng f & A >= max z holds
(low_toler (f,A)) [*] = low_toler (f,A)
let A be Real; :: 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 :: thesis: for p being object st p in (low_toler (f,A)) [*] holds
p in low_toler (f,A)

let p be object ; :: 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 object 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;
hence (low_toler (f,A)) [*] = low_toler (f,A) by XBOOLE_0:def 10; :: thesis: verum