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 A4: x in X ; :: thesis: X = Class R,x
reconsider x' = x as Element of X by A4;

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 x1' = x1 as Element of X ;
f . x1',x' <= A by A1, Th26;
then A5: [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, A5, 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 A6: a in {X} ; :: thesis: a in Class R
A7: a = X by A6, TARSKI:def 1;
consider x being set such that
A8: x in X by XBOOLE_0:def 1;
X = Class R,x by A3, A8;
hence a in Class R by A7, A8, EQREL_1:def 5; :: thesis: verum

end;

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

now

let a be set ; :: thesis: ( a in Class R implies a in {X} )
assume A10: a in Class R ; :: thesis: a in {X}
consider x being set such that
A11: ( x in X & a = Class R,x ) by A10, EQREL_1:def 5;
a = X by A3, A11;
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 A9, 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