let L be non empty satisfying_DN_1 ComplLLattStr ; :: thesis: for x, y being Element of L holds ((x + y) `) + x = x + (y `)

let x, y be Element of L; :: thesis: ((x + y) `) + x = x + (y `)

set Z = x;

x + ((y + ((((x + y) `) + x) `)) `) = ((x + y) `) + x by Th38;

hence ((x + y) `) + x = x + (y `) by Th28; :: thesis: verum

let x, y be Element of L; :: thesis: ((x + y) `) + x = x + (y `)

set Z = x;

x + ((y + ((((x + y) `) + x) `)) `) = ((x + y) `) + x by Th38;

hence ((x + y) `) + x = x + (y `) by Th28; :: thesis: verum