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

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