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

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