let L be non empty satisfying_DN_1 ComplLLattStr ; :: thesis: for x being Element of L holds (((x + (x `)) `) + x) ` = x `
let x be Element of L; :: thesis: (((x + (x `)) `) + x) ` = x `
set y = the Element of L;
set V = (x + the Element of L) ` ;
(((x + (x `)) `) + ((((((((x `) `) + the Element of L) `) + x) `) + ((((x `) `) + (((x `) + ((x + the Element of L) `)) `)) `)) `)) ` = x ` by Th1;
hence (((x + (x `)) `) + x) ` = x ` by Def1; :: thesis: verum