let i be set ; :: thesis: for I being non empty set
for EqR being Equivalence_Relation of I
for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds
c1 = c2
let I be non empty set ; :: thesis: for EqR being Equivalence_Relation of I
for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds
c1 = c2
let EqR be Equivalence_Relation of I; :: thesis: for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds
c1 = c2
let c1, c2 be Element of Class EqR; :: thesis: ( i in c1 & i in c2 implies c1 = c2 )
assume that
A1: i in c1 and
A2: i in c2 ; :: thesis: c1 = c2
consider x1 being object such that
x1 in I and
A3: c1 = Class (EqR,x1) by EQREL_1:def 3;
A4: [i,x1] in EqR by A1, A3, EQREL_1:19;
consider x2 being object such that
x2 in I and
A5: c2 = Class (EqR,x2) by EQREL_1:def 3;
[i,x2] in EqR by A2, A5, EQREL_1:19;
then Class (EqR,x2) = Class (EqR,i) by A1, EQREL_1:35
.= c1 by A1, A3, A4, EQREL_1:35 ;
hence c1 = c2 by A5; :: thesis: verum