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