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
thus EqR1 /\ (EqR1 "\/" EqR2) c= EqR1 by PBOOLE:17; :: according to PBOOLE:def 13 :: thesis: EqR1 c= EqR1 /\ (EqR1 "\/" EqR2)
A1: EqR1 c= EqR1 \/ EqR2 by PBOOLE:16;
EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Th6;
then EqR1 c= EqR1 "\/" EqR2 by A1, PBOOLE:15;
hence EqR1 c= EqR1 /\ (EqR1 "\/" EqR2) by PBOOLE:19; :: thesis: verum