for x being set st x in X holds
[x,x] in EqR2 by Th11;
then A1: id X c= EqR2 by RELAT_1:73;
for x being set st x in X holds
[x,x] in EqR1 by Th11;
then id X c= EqR1 by RELAT_1:73;
then id X c= EqR1 /\ EqR2 by A1, XBOOLE_1:19;
then ( dom (EqR1 /\ EqR2) = X & rng (EqR1 /\ EqR2) = X ) by RELSET_1:31, RELSET_1:32;
then A2: field (EqR1 /\ EqR2) = X ;
( EqR1 /\ EqR2 is symmetric & EqR1 /\ EqR2 is transitive ) by RELAT_2:35, RELAT_2:43;
hence EqR1 /\ EqR2 is Equivalence_Relation of X by A2, Th16; :: thesis: verum