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