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