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
( EqR1 = EqR1 \/ (EqR1 /\ EqR2) & ( for EqR being Equivalence_Relation of X st EqR1 \/ (EqR1 /\ EqR2) c= EqR holds
EqR1 c= EqR ) ) by XBOOLE_1:22;
hence EqR1 "\/" (EqR1 /\ EqR2) = EqR1 by Def2; :: thesis: verum