let X be set ; :: thesis: for EqR1, EqR2, EqR3 being Equivalence_Relation of X holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)

let EqR1, EqR2, EqR3 be Equivalence_Relation of X; :: thesis: (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)

for EqR4 being Equivalence_Relation of X st EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) holds

(EqR1 "\/" EqR2) "\/" EqR3 c= EqR4

for EqR4 being Equivalence_Relation of X st EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 holds

EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4

hence (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) by A6; :: thesis: verum

let EqR1, EqR2, EqR3 be Equivalence_Relation of X; :: thesis: (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)

for EqR4 being Equivalence_Relation of X st EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) holds

(EqR1 "\/" EqR2) "\/" EqR3 c= EqR4

proof

then A6:
(EqR1 "\/" EqR2) "\/" EqR3 c= EqR1 "\/" (EqR2 "\/" EqR3)
;
let EqR4 be Equivalence_Relation of X; :: thesis: ( EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) implies (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 )

A1: EqR2 \/ EqR3 c= EqR2 "\/" EqR3 by Def2;

assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) ; :: thesis: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4

then A2: EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by Def2;

EqR2 "\/" EqR3 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;

then EqR2 "\/" EqR3 c= EqR4 by A2;

then A3: EqR2 \/ EqR3 c= EqR4 by A1;

EqR2 c= EqR2 \/ EqR3 by XBOOLE_1:7;

then A4: EqR2 c= EqR4 by A3;

EqR1 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;

then EqR1 c= EqR4 by A2;

then EqR1 \/ EqR2 c= EqR4 by A4, XBOOLE_1:8;

then A5: EqR1 "\/" EqR2 c= EqR4 by Def2;

EqR3 c= EqR2 \/ EqR3 by XBOOLE_1:7;

then EqR3 c= EqR4 by A3;

then (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by A5, XBOOLE_1:8;

hence (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 by Def2; :: thesis: verum

end;A1: EqR2 \/ EqR3 c= EqR2 "\/" EqR3 by Def2;

assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) ; :: thesis: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4

then A2: EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by Def2;

EqR2 "\/" EqR3 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;

then EqR2 "\/" EqR3 c= EqR4 by A2;

then A3: EqR2 \/ EqR3 c= EqR4 by A1;

EqR2 c= EqR2 \/ EqR3 by XBOOLE_1:7;

then A4: EqR2 c= EqR4 by A3;

EqR1 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;

then EqR1 c= EqR4 by A2;

then EqR1 \/ EqR2 c= EqR4 by A4, XBOOLE_1:8;

then A5: EqR1 "\/" EqR2 c= EqR4 by Def2;

EqR3 c= EqR2 \/ EqR3 by XBOOLE_1:7;

then EqR3 c= EqR4 by A3;

then (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by A5, XBOOLE_1:8;

hence (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 by Def2; :: thesis: verum

for EqR4 being Equivalence_Relation of X st EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 holds

EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4

proof

then
EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3
;
let EqR4 be Equivalence_Relation of X; :: thesis: ( EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 implies EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 )

A7: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2;

assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 ; :: thesis: EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4

then A8: (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by Def2;

EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;

then EqR1 "\/" EqR2 c= EqR4 by A8;

then A9: EqR1 \/ EqR2 c= EqR4 by A7;

EqR3 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;

then A10: EqR3 c= EqR4 by A8;

EqR2 c= EqR1 \/ EqR2 by XBOOLE_1:7;

then EqR2 c= EqR4 by A9;

then EqR2 \/ EqR3 c= EqR4 by A10, XBOOLE_1:8;

then A11: EqR2 "\/" EqR3 c= EqR4 by Def2;

EqR1 c= EqR1 \/ EqR2 by XBOOLE_1:7;

then EqR1 c= EqR4 by A9;

then EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by A11, XBOOLE_1:8;

hence EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 by Def2; :: thesis: verum

end;A7: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2;

assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 ; :: thesis: EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4

then A8: (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by Def2;

EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;

then EqR1 "\/" EqR2 c= EqR4 by A8;

then A9: EqR1 \/ EqR2 c= EqR4 by A7;

EqR3 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;

then A10: EqR3 c= EqR4 by A8;

EqR2 c= EqR1 \/ EqR2 by XBOOLE_1:7;

then EqR2 c= EqR4 by A9;

then EqR2 \/ EqR3 c= EqR4 by A10, XBOOLE_1:8;

then A11: EqR2 "\/" EqR3 c= EqR4 by Def2;

EqR1 c= EqR1 \/ EqR2 by XBOOLE_1:7;

then EqR1 c= EqR4 by A9;

then EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by A11, XBOOLE_1:8;

hence EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 by Def2; :: thesis: verum

hence (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) by A6; :: thesis: verum