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