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
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 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 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; :: 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 :: thesis: for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}

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 :: thesis: for x1 being object st x1 in X holds
x1 in Class (R,x)

let x1 be object ; :: 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:19; :: thesis: verum

end;

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

end;

now :: thesis: for a being object st a in {X} holds
a in Class R

let a be object ; :: 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 object 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 3; :: thesis: verum

end;

then A7: {X} c= Class R ;

now :: thesis: for a being object st a in Class R holds
a in {X}

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

end;

then Class R c= {X} ;
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