let I be non empty set ; :: thesis: for M being ManySortedSet of
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 \/ EqR2 c= EqR1 "\/" EqR2
let M be ManySortedSet of ; :: thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 \/ EqR2 c= EqR1 "\/" EqR2
let EqR1, EqR2 be Equivalence_Relation of M; :: thesis: EqR1 \/ EqR2 c= EqR1 "\/" EqR2
consider EqR3 being ManySortedRelation of M such that
A1: ( EqR3 = EqR1 \/ EqR2 & EqR1 "\/" EqR2 = EqCl EqR3 ) by Def4;

now

let i be set ; :: thesis: ( i in I implies EqR3 . i c= (EqR1 "\/" EqR2) . i )
assume i in I ; :: thesis: EqR3 . i c= (EqR1 "\/" EqR2) . i
then reconsider i' = i as Element of I ;
EqR3 . i c= EqCl (EqR3 . i') by Def1;
hence EqR3 . i c= (EqR1 "\/" EqR2) . i by A1, Def3; :: thesis: verum

end;

hence EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by A1, PBOOLE:def 5; :: thesis: verum