let a, b, c be Element of (CLatt L); :: according to LATTICES:def 5 :: thesis: a + (b + c) = (a + b) + c
set K = the L_join of L;
set M = the L_join of (CLatt L);
A1: the carrier of L = the carrier of (CLatt L) by Def11;
the L_join of L = the L_join of (CLatt L) by Def11;
hence a + (b + c) = (a + b) + c by A1, BINOP_1:def 3; :: thesis: verum