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

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

let i be object ; :: thesis: ( i in I implies (EqR1 "\/" EqR2) . i c= EqR . i )
assume A4: i in I ; :: thesis: (EqR1 "\/" EqR2) . i c= EqR . i
then reconsider i9 = i as Element of I ;
EqR . i9 is Relation of (M . i) ;
then reconsider E = EqR . i as Equivalence_Relation of (M . i) by MSUALG_4:def 2;
EqR3 . i c= E by A3, A1, A4, PBOOLE:def 2;
then EqCl (EqR3 . i9) 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 2; :: thesis: verum