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