let X be set ; :: thesis: for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1
let EqR1, EqR2 be Equivalence_Relation of X; :: thesis: EqR1 /\ (EqR1 "\/" EqR2) = EqR1
thus EqR1 /\ (EqR1 "\/" EqR2) c= EqR1 by XBOOLE_1:17; :: according to XBOOLE_0:def 10 :: thesis: EqR1 c= EqR1 /\ (EqR1 "\/" EqR2)
( EqR1 c= EqR1 \/ EqR2 & EqR1 \/ EqR2 c= EqR1 "\/" EqR2 ) by Def2, XBOOLE_1:7;
then EqR1 c= EqR1 "\/" EqR2 ;
hence EqR1 c= EqR1 /\ (EqR1 "\/" EqR2) by XBOOLE_1:19; :: thesis: verum