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