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