for x being set st x in X holds
[x,x] in EqR2 by Th11;
then A1: id X c= EqR2 by RELAT_1:47;
for x being set st x in X holds
[x,x] in EqR1 by Th11;
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, RELSET_1:17;
then A2: field (EqR1 /\ EqR2) = X ;
( EqR1 /\ EqR2 is symmetric & EqR1 /\ EqR2 is transitive ) by RELAT_2:18, RELAT_2:26;
hence EqR1 /\ EqR2 is Equivalence_Relation of X by A2, Th16; :: thesis: verum