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

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