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