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