let L be non empty satisfying_DN_1 ComplLattStr ; :: 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 X = (y + x) ` ;
(((y + x) ` ) + (((((x ` ) + y) ` ) + (((x ` ) + ((y + x) ` )) ` )) ` )) ` = x by Th13;
hence ((x ` ) + ((y + x) ` )) ` = x by Th10; :: thesis: verum