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

now

let i be set ; :: thesis: ( i in I implies (EqR1 "\/" EqR2) . i c= EqR . i )
assume A3: i in I ; :: thesis: (EqR1 "\/" EqR2) . i c= EqR . i
then reconsider i' = i as Element of I ;
EqR . i' is Relation of (M . i) ;
then reconsider E = EqR . i as Equivalence_Relation of (M . i) by MSUALG_4:def 3;
EqR3 . i c= E by A1, A2, A3, PBOOLE:def 5;
then EqCl (EqR3 . i') c= E by Def1;
hence (EqR1 "\/" EqR2) . i c= EqR . i by A2, Def3; :: thesis: verum

end;

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