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 Th72;

A2: now

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

now

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 Th55;
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, Th55;
reconsider d = b \/ (b1 \/ c1) as Element of DISJOINT_PAIRS A by A5, A8;
A9: b \/ (b1 \/ c1) = (b \/ b1) \/ c1 by Th16;
then b \/ b1 c= d by Th26;
then reconsider c2 = b \/ b1 as Element of DISJOINT_PAIRS A by Th45;
c2 in K ^ L by A3, A6, Th56;
hence a in (K ^ L) ^ M by A5, A7, A8, A9, Th56; :: thesis: verum

end;

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

end;

then A10: K ^ (L ^ M) c= (K ^ L) ^ M ;
( (K ^ L) ^ M = M ^ (K ^ L) & K ^ (L ^ M) = (L ^ M) ^ K ) by Th72;
then (K ^ L) ^ M c= K ^ (L ^ M) by A1, A2;
hence K ^ (L ^ M) = (K ^ L) ^ M by A10, XBOOLE_0:def 10; :: thesis: verum