let x, y be Element of (CLatt L); :: according to ROBBINS1:def 6 :: thesis: (((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = x
reconsider x' = x, y' = y as Element of L by Def11;
A1: ( x ` = x' ` & y ` = y' ` ) by Def11;
then (x ` ) + (y ` ) = (x' ` ) + (y' ` ) by Def11;
then A2: ((x ` ) + (y ` )) ` = ((x' ` ) + (y' ` )) ` by Def11;
(x ` ) + y = (x' ` ) + y' by A1, Def11;
then ((x ` ) + y) ` = ((x' ` ) + y') ` by Def11;
hence (((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = (((x' ` ) + (y' ` )) ` ) + (((x' ` ) + y') ` ) by A2, Def11
.= x by Def6 ;
:: thesis: verum