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

[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