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

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