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