let L be non empty satisfying_DN_1 ComplLLattStr ; :: thesis: for x, y, z being Element of L holds (x + y) + (x + z) = y + (x + z)
let x, y, z be Element of L; :: thesis: (x + y) + (x + z) = y + (x + z)
set Y = x;
set X = y;
((y `) `) + (x + z) = (x + y) + (x + z) by Th52;
hence (x + y) + (x + z) = y + (x + z) by Th23; :: thesis: verum