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