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