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