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

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