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

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