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 Z = x ` ;
set X = y;
set Y = x;
(((((y + x) ` ) + (x ` )) ` ) + ((y + (x ` )) ` )) ` = x ` by Th9;
hence (x + ((y + (x ` )) ` )) ` = x ` by Th19; :: thesis: verum