let a, b be Element of (CLatt L); :: according to LATTICES:def 4 :: thesis: a + b = b + a
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 = b + a by A1, BINOP_1:def 2; :: thesis: verum