let I be non empty set ; :: thesis: for M being ManySortedSet of I
for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
let M be ManySortedSet of I; :: 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: EqR2 (\/) EqR3 c= EqR2 "\/" EqR3 by Th4;
assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) ; :: thesis: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
then A2: EqR1 (\/) (EqR2 "\/" EqR3) c= EqR4 by Th4;
EqR2 "\/" EqR3 c= EqR1 (\/) (EqR2 "\/" EqR3) by PBOOLE:14;
then EqR2 "\/" EqR3 c= EqR4 by A2, PBOOLE:13;
then A3: EqR2 (\/) EqR3 c= EqR4 by A1, PBOOLE:13;
EqR2 c= EqR2 (\/) EqR3 by PBOOLE:14;
then A4: EqR2 c= EqR4 by A3, PBOOLE:13;
EqR1 c= EqR1 (\/) (EqR2 "\/" EqR3) by PBOOLE:14;
then EqR1 c= EqR4 by A2, PBOOLE:13;
then EqR1 (\/) EqR2 c= EqR4 by A4, PBOOLE:16;
then A5: EqR1 "\/" EqR2 c= EqR4 by Th5;
EqR3 c= EqR2 (\/) EqR3 by PBOOLE:14;
then EqR3 c= EqR4 by A3, PBOOLE:13;
then (EqR1 "\/" EqR2) (\/) EqR3 c= EqR4 by A5, PBOOLE:16;
hence (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 by Th5; :: thesis: verum
end;
then A6: (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 )
A7: EqR1 (\/) EqR2 c= EqR1 "\/" EqR2 by Th4;
assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 ; :: thesis: EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
then A8: (EqR1 "\/" EqR2) (\/) EqR3 c= EqR4 by Th4;
EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) (\/) EqR3 by PBOOLE:14;
then EqR1 "\/" EqR2 c= EqR4 by A8, PBOOLE:13;
then A9: EqR1 (\/) EqR2 c= EqR4 by A7, PBOOLE:13;
EqR3 c= (EqR1 "\/" EqR2) (\/) EqR3 by PBOOLE:14;
then A10: EqR3 c= EqR4 by A8, PBOOLE:13;
EqR2 c= EqR1 (\/) EqR2 by PBOOLE:14;
then EqR2 c= EqR4 by A9, PBOOLE:13;
then EqR2 (\/) EqR3 c= EqR4 by A10, PBOOLE:16;
then A11: EqR2 "\/" EqR3 c= EqR4 by Th5;
EqR1 c= EqR1 (\/) EqR2 by PBOOLE:14;
then EqR1 c= EqR4 by A9, PBOOLE:13;
then EqR1 (\/) (EqR2 "\/" EqR3) c= EqR4 by A11, PBOOLE:16;
hence EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 by Th5; :: thesis: verum
end;
then EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3 ;
hence (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) by A6, PBOOLE:146; :: thesis: verum