let R1, R2 be Equivalence_Relation of X; :: thesis: ( EqR1 \/ EqR2 c= R1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R1 c= EqR ) & EqR1 \/ EqR2 c= R2 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R2 c= EqR ) implies R1 = R2 )
assume ( EqR1 \/ EqR2 c= R1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R1 c= EqR ) & EqR1 \/ EqR2 c= R2 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R2 c= EqR ) ) ; :: thesis: R1 = R2
then ( R1 c= R2 & R2 c= R1 ) ;
hence R1 = R2 by XBOOLE_0:def 10; :: thesis: verum