let X be non empty set ; :: thesis: for E being Equivalence_Relation of X

for x, y being set

for C being Element of Class E st x in C & y in C holds

[x,y] in E

let E be Equivalence_Relation of X; :: thesis: for x, y being set

for C being Element of Class E st x in C & y in C holds

[x,y] in E

let x, y be set ; :: thesis: for C being Element of Class E st x in C & y in C holds

[x,y] in E

let C be Element of Class E; :: thesis: ( x in C & y in C implies [x,y] in E )

assume A1: ( x in C & y in C ) ; :: thesis: [x,y] in E

reconsider EE = E as transitive Tolerance of X ;

consider xe being object such that

A2: ( xe in X & C = Class (E,xe) ) by EQREL_1:def 3;

thus [x,y] in E by EQREL_1:22, A1, A2; :: thesis: verum

for x, y being set

for C being Element of Class E st x in C & y in C holds

[x,y] in E

let E be Equivalence_Relation of X; :: thesis: for x, y being set

for C being Element of Class E st x in C & y in C holds

[x,y] in E

let x, y be set ; :: thesis: for C being Element of Class E st x in C & y in C holds

[x,y] in E

let C be Element of Class E; :: thesis: ( x in C & y in C implies [x,y] in E )

assume A1: ( x in C & y in C ) ; :: thesis: [x,y] in E

reconsider EE = E as transitive Tolerance of X ;

consider xe being object such that

A2: ( xe in X & C = Class (E,xe) ) by EQREL_1:def 3;

thus [x,y] in E by EQREL_1:22, A1, A2; :: thesis: verum