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