let L be non empty satisfying_DN_1 ComplLattStr ; :: 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