let L be non empty satisfying_DN_1 ComplLLattStr ; :: thesis: for x, y, z being Element of L holds x + (((y + (x `)) + z) `) = x
let x, y, z be Element of L; :: thesis: x + (((y + (x `)) + z) `) = x
(((((y + (x `)) + z) `) + x) `) ` = x by Th41;
hence x + (((y + (x `)) + z) `) = x by Th25; :: thesis: verum