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

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