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