let I be non empty set ; :: thesis: for M being ManySortedSet of I
for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR = EqR1 (/\) EqR2 holds
EqR1 "\/" EqR = EqR1
let M be ManySortedSet of I; :: thesis: for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR = EqR1 (/\) EqR2 holds
EqR1 "\/" EqR = EqR1
let EqR1, EqR2 be Equivalence_Relation of M; :: thesis: for EqR being Equivalence_Relation of M st EqR = EqR1 (/\) EqR2 holds
EqR1 "\/" EqR = EqR1
A1: EqR1 = EqR1 (\/) (EqR1 (/\) EqR2) by PBOOLE:31;
A2: for EqR4 being Equivalence_Relation of M st EqR1 (\/) (EqR1 (/\) EqR2) c= EqR4 holds
EqR1 c= EqR4 by PBOOLE:31;
let EqR be Equivalence_Relation of M; :: thesis: ( EqR = EqR1 (/\) EqR2 implies EqR1 "\/" EqR = EqR1 )
assume EqR = EqR1 (/\) EqR2 ; :: thesis: EqR1 "\/" EqR = EqR1
hence EqR1 "\/" EqR = EqR1 by A1, A2, Th6; :: thesis: verum