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
for R being Equivalence_Relation of X st R = (low_toler f,A) [*] holds
Class R = {X}
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
for R being Equivalence_Relation of X st R = (low_toler f,A) [*] holds
Class R = {X}
let z be non empty finite Subset of REAL ; :: thesis: for A being real number st z = rng f & A >= max z holds
for R being Equivalence_Relation of X st R = (low_toler f,A) [*] holds
Class R = {X}
let A be real number ; :: thesis: ( z = rng f & A >= max z implies for R being Equivalence_Relation of X st R = (low_toler f,A) [*] holds
Class R = {X} )
assume A1: ( z = rng f & A >= max z ) ; :: thesis: for R being Equivalence_Relation of X st R = (low_toler f,A) [*] holds
Class R = {X}

now

let R be Equivalence_Relation of X; :: thesis: ( R = (low_toler f,A) [*] implies Class R = {X} )
assume A2: R = (low_toler f,A) [*] ; :: thesis: Class R = {X}
A3: for x being set st x in X holds
X = Class R,x

proof

let x be set ; :: thesis: ( x in X implies X = Class R,x )
assume x in X ; :: thesis: X = Class R,x
then reconsider x9 = x as Element of X ;

now

let x1 be set ; :: thesis: ( x1 in X implies x1 in Class R,x )
assume x1 in X ; :: thesis: x1 in Class R,x
then reconsider x19 = x1 as Element of X ;
f . x19,x9 <= A by A1, Th26;
then A4: [x1,x] in low_toler f,A by Def3;
low_toler f,A c= (low_toler f,A) [*] by LANG1:18;
hence x1 in Class R,x by A2, A4, EQREL_1:27; :: thesis: verum

end;

then X c= Class R,x by TARSKI:def 3;
hence X = Class R,x by XBOOLE_0:def 10; :: thesis: verum

end;

now

let a be set ; :: thesis: ( a in {X} implies a in Class R )
assume a in {X} ; :: thesis: a in Class R
then A5: a = X by TARSKI:def 1;
consider x being set such that
A6: x in X by XBOOLE_0:def 1;
X = Class R,x by A3, A6;
hence a in Class R by A5, A6, EQREL_1:def 5; :: thesis: verum

end;

then A7: {X} c= Class R by TARSKI:def 3;

now

let a be set ; :: thesis: ( a in Class R implies a in {X} )
assume a in Class R ; :: thesis: a in {X}
then ex x being set st
( x in X & a = Class R,x ) by EQREL_1:def 5;
then a = X by A3;
hence a in {X} by TARSKI:def 1; :: thesis: verum

end;

then Class R c= {X} by TARSKI:def 3;
hence Class R = {X} by A7, XBOOLE_0:def 10; :: thesis: verum

end;

hence for R being Equivalence_Relation of X st R = (low_toler f,A) [*] holds
Class R = {X} ; :: thesis: verum