let I be non empty set ; :: thesis: for M being ManySortedSet of
for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
let M be ManySortedSet of ; :: thesis: for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
let EqR1, EqR2, EqR3 be Equivalence_Relation of M; :: thesis: (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
for EqR4 being Equivalence_Relation of M st EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 holds
EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4

proof

let EqR4 be Equivalence_Relation of M; :: thesis: ( EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 implies EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 )
A1: EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) \/ EqR3 by PBOOLE:16;
A2: EqR3 c= (EqR1 "\/" EqR2) \/ EqR3 by PBOOLE:16;
A3: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Th6;
A4: ( EqR1 c= EqR1 \/ EqR2 & EqR2 c= EqR1 \/ EqR2 ) by PBOOLE:16;
assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 ; :: thesis: EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
then A5: (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by Th6;
then EqR1 "\/" EqR2 c= EqR4 by A1, PBOOLE:15;
then EqR1 \/ EqR2 c= EqR4 by A3, PBOOLE:15;
then A6: ( EqR1 c= EqR4 & EqR2 c= EqR4 & EqR3 c= EqR4 ) by A2, A4, A5, PBOOLE:15;
then EqR2 \/ EqR3 c= EqR4 by PBOOLE:18;
then EqR2 "\/" EqR3 c= EqR4 by Th7;
then EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by A6, PBOOLE:18;
hence EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 by Th7; :: thesis: verum

end;

then A7: EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3 ;
for EqR4 being Equivalence_Relation of M st EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) holds
(EqR1 "\/" EqR2) "\/" EqR3 c= EqR4

proof

let EqR4 be Equivalence_Relation of M; :: thesis: ( EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) implies (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 )
A8: EqR2 "\/" EqR3 c= EqR1 \/ (EqR2 "\/" EqR3) by PBOOLE:16;
A9: EqR1 c= EqR1 \/ (EqR2 "\/" EqR3) by PBOOLE:16;
A10: EqR2 \/ EqR3 c= EqR2 "\/" EqR3 by Th6;
A11: ( EqR2 c= EqR2 \/ EqR3 & EqR3 c= EqR2 \/ EqR3 ) by PBOOLE:16;
assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) ; :: thesis: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
then A12: EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by Th6;
then EqR2 "\/" EqR3 c= EqR4 by A8, PBOOLE:15;
then EqR2 \/ EqR3 c= EqR4 by A10, PBOOLE:15;
then A13: ( EqR1 c= EqR4 & EqR2 c= EqR4 & EqR3 c= EqR4 ) by A9, A11, A12, PBOOLE:15;
then EqR1 \/ EqR2 c= EqR4 by PBOOLE:18;
then EqR1 "\/" EqR2 c= EqR4 by Th7;
then (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by A13, PBOOLE:18;
hence (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 by Th7; :: thesis: verum

end;

then (EqR1 "\/" EqR2) "\/" EqR3 c= EqR1 "\/" (EqR2 "\/" EqR3) ;
hence (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) by A7, PBOOLE:def 13; :: thesis: verum