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
((x + y) `) ` = ((y + x) `) ` by Th14
.= y + x by Th23 ;
hence ((x + y) `) ` = y + x ; :: thesis: verum