let I be non empty set ; :: thesis: for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 (\/) EqR2 c= EqR1 "\/" EqR2
let M be ManySortedSet of I; :: 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 and
A2: EqR1 "\/" EqR2 = EqCl EqR3 by Def4;

now :: thesis: for i being object st i in I holds
EqR3 . i c= (EqR1 "\/" EqR2) . i

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

end;

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