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