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

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