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