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

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