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) ` ;
set Y = y ` ;
((x + y) ` ) + (((((y ` ) + ((x + y) ` )) ` ) + (y ` )) ` ) = (x + y) ` by Th28;
hence ((x + y) ` ) + ((y + (y ` )) ` ) = (x + y) ` by Th18; :: thesis: verum