let I be non empty set ; :: thesis: for M being ManySortedSet of I

for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds

EqR3 c= EqR ) holds

EqR3 = EqR1 "\/" EqR2

let M be ManySortedSet of I; :: thesis: for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds

EqR3 c= EqR ) holds

EqR3 = EqR1 "\/" EqR2

let EqR1, EqR2, EqR3 be Equivalence_Relation of M; :: thesis: ( EqR1 (\/) EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds

EqR3 c= EqR ) implies EqR3 = EqR1 "\/" EqR2 )

assume that

A1: EqR1 (\/) EqR2 c= EqR3 and

A2: for EqR being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds

EqR3 c= EqR ; :: thesis: EqR3 = EqR1 "\/" EqR2

A3: EqR1 "\/" EqR2 c= EqR3 by A1, Th5;

EqR3 c= EqR1 "\/" EqR2 by A2, Th4;

hence EqR3 = EqR1 "\/" EqR2 by A3, PBOOLE:146; :: thesis: verum

for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds

EqR3 c= EqR ) holds

EqR3 = EqR1 "\/" EqR2

let M be ManySortedSet of I; :: thesis: for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds

EqR3 c= EqR ) holds

EqR3 = EqR1 "\/" EqR2

let EqR1, EqR2, EqR3 be Equivalence_Relation of M; :: thesis: ( EqR1 (\/) EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds

EqR3 c= EqR ) implies EqR3 = EqR1 "\/" EqR2 )

assume that

A1: EqR1 (\/) EqR2 c= EqR3 and

A2: for EqR being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds

EqR3 c= EqR ; :: thesis: EqR3 = EqR1 "\/" EqR2

A3: EqR1 "\/" EqR2 c= EqR3 by A1, Th5;

EqR3 c= EqR1 "\/" EqR2 by A2, Th4;

hence EqR3 = EqR1 "\/" EqR2 by A3, PBOOLE:146; :: thesis: verum