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