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