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