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}

Class R = {X} ; :: thesis: verum

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}

hence
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)

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

end;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 ;

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

end;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)

then
X c= Class (R,x)
;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;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

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

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

a in Class R

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

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

a in {X}

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

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

Class R = {X} ; :: thesis: verum