let I be non empty set ; :: thesis: for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 (/\) EqR2 is Equivalence_Relation of M
let M be ManySortedSet of I; :: thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 (/\) EqR2 is Equivalence_Relation of M
let EqR1, EqR2 be Equivalence_Relation of M; :: thesis: EqR1 (/\) EqR2 is Equivalence_Relation of M
for i being set st i in I holds
(EqR1 (/\) EqR2) . i is Relation of (M . i),(M . i)

proof

let i be set ; :: thesis: ( i in I implies (EqR1 (/\) EqR2) . i is Relation of (M . i),(M . i) )
assume A1: i in I ; :: thesis: (EqR1 (/\) EqR2) . i is Relation of (M . i),(M . i)
then reconsider U19 = EqR1 . i as Relation of (M . i),(M . i) by MSUALG_4:def 1;
reconsider U29 = EqR2 . i as Relation of (M . i),(M . i) by A1, MSUALG_4:def 1;
(EqR1 (/\) EqR2) . i = U19 /\ U29 by A1, PBOOLE:def 5;
hence (EqR1 (/\) EqR2) . i is Relation of (M . i),(M . i) ; :: thesis: verum

end;

then reconsider U3 = EqR1 (/\) EqR2 as ManySortedRelation of M by MSUALG_4:def 1;
for i being object
for R being Relation of (M . i) st i in I & U3 . i = R holds
R is Equivalence_Relation of (M . i)

proof

let i be object ; :: thesis: for R being Relation of (M . i) st i in I & U3 . i = R holds
R is Equivalence_Relation of (M . i)
let R be Relation of (M . i); :: thesis: ( i in I & U3 . i = R implies R is Equivalence_Relation of (M . i) )
assume that
A2: i in I and
A3: U3 . i = R ; :: thesis: R is Equivalence_Relation of (M . i)
reconsider U29 = EqR2 . i as Relation of (M . i) by A2, MSUALG_4:def 1;
reconsider U29 = U29 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def 2;
reconsider U19 = EqR1 . i as Relation of (M . i) by A2, MSUALG_4:def 1;
reconsider U19 = U19 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def 2;
U19 /\ U29 is Equivalence_Relation of (M . i) ;
hence R is Equivalence_Relation of (M . i) by A2, A3, PBOOLE:def 5; :: thesis: verum

end;

hence EqR1 (/\) EqR2 is Equivalence_Relation of M by MSUALG_4:def 2; :: thesis: verum