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