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)
( EqR1 \/ EqR2 c= EqR1 "\/" EqR2 & ( for EqR3 being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR3 holds
EqR1 "\/" EqR2 c= EqR3 ) ) by EQREL_1:def 3;
hence EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2) by Def1; :: thesis: verum