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