let C1, C2 be Equivalence_Relation of X; :: thesis: ( R c= C1 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

C1 c= EqR2 ) & R c= C2 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

C2 c= EqR2 ) implies C1 = C2 )

assume that

A1: R c= C1 and

A2: for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

C1 c= EqR2 and

A3: R c= C2 and

A4: for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

C2 c= EqR2 ; :: thesis: C1 = C2

A5: C2 c= C1 by A1, A4;

C1 c= C2 by A2, A3;

hence C1 = C2 by A5, XBOOLE_0:def 10; :: thesis: verum

C1 c= EqR2 ) & R c= C2 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

C2 c= EqR2 ) implies C1 = C2 )

assume that

A1: R c= C1 and

A2: for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

C1 c= EqR2 and

A3: R c= C2 and

A4: for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

C2 c= EqR2 ; :: thesis: C1 = C2

A5: C2 c= C1 by A1, A4;

C1 c= C2 by A2, A3;

hence C1 = C2 by A5, XBOOLE_0:def 10; :: thesis: verum