let I be non empty set ; :: thesis: for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 (/\) (EqR1 "\/" EqR2) = EqR1
let M be ManySortedSet of I; :: thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 (/\) (EqR1 "\/" EqR2) = EqR1
let EqR1, EqR2 be Equivalence_Relation of M; :: thesis: EqR1 (/\) (EqR1 "\/" EqR2) = EqR1
A1: EqR1 (/\) (EqR1 "\/" EqR2) c= EqR1 by PBOOLE:15;
A2: EqR1 c= EqR1 (\/) EqR2 by PBOOLE:14;
EqR1 (\/) EqR2 c= EqR1 "\/" EqR2 by Th4;
then EqR1 c= EqR1 "\/" EqR2 by A2, PBOOLE:13;
then EqR1 c= EqR1 (/\) (EqR1 "\/" EqR2) by PBOOLE:17;
hence EqR1 (/\) (EqR1 "\/" EqR2) = EqR1 by A1, PBOOLE:146; :: thesis: verum