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