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