let L be non empty satisfying_DN_1 ComplLLattStr ; :: thesis: for x, y, z being Element of L holds x + ((y + ((((z + y) `) + x) `)) `) = ((z + y) `) + x
let x, y, z be Element of L; :: thesis: x + ((y + ((((z + y) `) + x) `)) `) = ((z + y) `) + x
set Y = (z + y) ` ;
set Z = y ` ;
x + ((((((z + y) `) + (y `)) `) + ((((z + y) `) + x) `)) `) = ((z + y) `) + x by Th37;
hence x + ((y + ((((z + y) `) + x) `)) `) = ((z + y) `) + x by Th19; :: thesis: verum