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 Z = x ` ;
set X = y;
set Y = x;
(((((y + x) `) + (x `)) `) + ((y + (x `)) `)) ` = x ` by Th9;
hence (x + ((y + (x `)) `)) ` = x ` by Th19; :: thesis: verum