let A be set ; :: thesis: for K, L, M being Element of Normal_forms_on A holds K ^ (L ^ M) = (K ^ L) ^ M

let K, L, M be Element of Normal_forms_on A; :: thesis: K ^ (L ^ M) = (K ^ L) ^ M

A1: ( L ^ M = M ^ L & K ^ L = L ^ K ) by Th48;

( (K ^ L) ^ M = M ^ (K ^ L) & K ^ (L ^ M) = (L ^ M) ^ K ) by Th48;

then (K ^ L) ^ M c= K ^ (L ^ M) by A1, A2;

hence K ^ (L ^ M) = (K ^ L) ^ M by A10; :: thesis: verum

let K, L, M be Element of Normal_forms_on A; :: thesis: K ^ (L ^ M) = (K ^ L) ^ M

A1: ( L ^ M = M ^ L & K ^ L = L ^ K ) by Th48;

A2: now :: thesis: for K, L, M being Element of Normal_forms_on A holds K ^ (L ^ M) c= (K ^ L) ^ M

then A10:
K ^ (L ^ M) c= (K ^ L) ^ M
;let K, L, M be Element of Normal_forms_on A; :: thesis: K ^ (L ^ M) c= (K ^ L) ^ M

end;now :: thesis: for a being Element of DISJOINT_PAIRS A st a in K ^ (L ^ M) holds

a in (K ^ L) ^ M

hence
K ^ (L ^ M) c= (K ^ L) ^ M
by Lm5; :: thesis: veruma in (K ^ L) ^ M

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in K ^ (L ^ M) implies a in (K ^ L) ^ M )

assume a in K ^ (L ^ M) ; :: thesis: a in (K ^ L) ^ M

then consider b, c being Element of DISJOINT_PAIRS A such that

A3: b in K and

A4: c in L ^ M and

A5: a = b \/ c by Th34;

consider b1, c1 being Element of DISJOINT_PAIRS A such that

A6: b1 in L and

A7: c1 in M and

A8: c = b1 \/ c1 by A4, Th34;

reconsider d = b \/ (b1 \/ c1) as Element of DISJOINT_PAIRS A by A5, A8;

A9: b \/ (b1 \/ c1) = (b \/ b1) \/ c1 by Th3;

then b \/ b1 c= d by Th10;

then reconsider c2 = b \/ b1 as Element of DISJOINT_PAIRS A by Th26;

c2 in K ^ L by A3, A6, Th35;

hence a in (K ^ L) ^ M by A5, A7, A8, A9, Th35; :: thesis: verum

end;assume a in K ^ (L ^ M) ; :: thesis: a in (K ^ L) ^ M

then consider b, c being Element of DISJOINT_PAIRS A such that

A3: b in K and

A4: c in L ^ M and

A5: a = b \/ c by Th34;

consider b1, c1 being Element of DISJOINT_PAIRS A such that

A6: b1 in L and

A7: c1 in M and

A8: c = b1 \/ c1 by A4, Th34;

reconsider d = b \/ (b1 \/ c1) as Element of DISJOINT_PAIRS A by A5, A8;

A9: b \/ (b1 \/ c1) = (b \/ b1) \/ c1 by Th3;

then b \/ b1 c= d by Th10;

then reconsider c2 = b \/ b1 as Element of DISJOINT_PAIRS A by Th26;

c2 in K ^ L by A3, A6, Th35;

hence a in (K ^ L) ^ M by A5, A7, A8, A9, Th35; :: thesis: verum

( (K ^ L) ^ M = M ^ (K ^ L) & K ^ (L ^ M) = (L ^ M) ^ K ) by Th48;

then (K ^ L) ^ M c= K ^ (L ^ M) by A1, A2;

hence K ^ (L ^ M) = (K ^ L) ^ M by A10; :: thesis: verum