let X be set ; :: thesis: for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2)
let EqR1, EqR2 be Equivalence_Relation of X; :: thesis: EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2)
A1: for EqR3 being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR3 holds
EqR1 "\/" EqR2 c= EqR3 by EQREL_1:def 2;
EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by EQREL_1:def 2;
hence EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2) by A1, Def1; :: thesis: verum