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