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

for C1, C2 being Element of Class E

for x1, x2 being set st x1 in C1 & x2 in C2 & [x1,x2] in E holds

C1 = C2

let E be Equivalence_Relation of X; :: thesis: for C1, C2 being Element of Class E

for x1, x2 being set st x1 in C1 & x2 in C2 & [x1,x2] in E holds

C1 = C2

let C1, C2 be Element of Class E; :: thesis: for x1, x2 being set st x1 in C1 & x2 in C2 & [x1,x2] in E holds

C1 = C2

let x1, x2 be set ; :: thesis: ( x1 in C1 & x2 in C2 & [x1,x2] in E implies C1 = C2 )

reconsider EE = E as Tolerance of X ;

assume A1: x1 in C1 ; :: thesis: ( not x2 in C2 or not [x1,x2] in E or C1 = C2 )

then reconsider x11 = x1 as Element of X ;

x11 in X ;

then x1 in Class (EE,x1) by EQREL_1:20;

then A2: C1 = EqClass (E,x11) by EQREL_1:def 4, A1, XBOOLE_0:3;

assume A3: x2 in C2 ; :: thesis: ( not [x1,x2] in E or C1 = C2 )

then reconsider x22 = x2 as Element of X ;

x22 in X ;

then x2 in Class (EE,x2) by EQREL_1:20;

then A4: C2 = EqClass (E,x22) by EQREL_1:def 4, A3, XBOOLE_0:3;

assume [x1,x2] in E ; :: thesis: C1 = C2

hence C1 = C2 by A2, A4, EQREL_1:35; :: thesis: verum

for C1, C2 being Element of Class E

for x1, x2 being set st x1 in C1 & x2 in C2 & [x1,x2] in E holds

C1 = C2

let E be Equivalence_Relation of X; :: thesis: for C1, C2 being Element of Class E

for x1, x2 being set st x1 in C1 & x2 in C2 & [x1,x2] in E holds

C1 = C2

let C1, C2 be Element of Class E; :: thesis: for x1, x2 being set st x1 in C1 & x2 in C2 & [x1,x2] in E holds

C1 = C2

let x1, x2 be set ; :: thesis: ( x1 in C1 & x2 in C2 & [x1,x2] in E implies C1 = C2 )

reconsider EE = E as Tolerance of X ;

assume A1: x1 in C1 ; :: thesis: ( not x2 in C2 or not [x1,x2] in E or C1 = C2 )

then reconsider x11 = x1 as Element of X ;

x11 in X ;

then x1 in Class (EE,x1) by EQREL_1:20;

then A2: C1 = EqClass (E,x11) by EQREL_1:def 4, A1, XBOOLE_0:3;

assume A3: x2 in C2 ; :: thesis: ( not [x1,x2] in E or C1 = C2 )

then reconsider x22 = x2 as Element of X ;

x22 in X ;

then x2 in Class (EE,x2) by EQREL_1:20;

then A4: C2 = EqClass (E,x22) by EQREL_1:def 4, A3, XBOOLE_0:3;

assume [x1,x2] in E ; :: thesis: C1 = C2

hence C1 = C2 by A2, A4, EQREL_1:35; :: thesis: verum