let L be non empty satisfying_DN_1 ComplLattStr ; :: 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