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

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