for x being object st x in X holds
[x,x] in EqR2 by Th5;
then A1: id X c= EqR2 by RELAT_1:47;
for x being object st x in X holds
[x,x] in EqR1 by Th5;
then id X c= EqR1 by RELAT_1:47;
then id X c= EqR1 /\ EqR2 by A1, XBOOLE_1:19;
then ( dom (EqR1 /\ EqR2) = X & rng (EqR1 /\ EqR2) = X ) by RELSET_1:16;
then field (EqR1 /\ EqR2) = X ;
hence EqR1 /\ EqR2 is Equivalence_Relation of X by Th9; :: thesis: verum