let L be non empty satisfying_DN_1 ComplLLattStr ; :: thesis: L is Robbins
for x, y being Element of L holds (((x + y) `) + ((x + (y `)) `)) ` = x by Th6;
hence L is Robbins by ROBBINS1:def 5; :: thesis: verum