theorem :: ROBBINS2:30

for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds x + ((((y + x) `) + y) `) = x by Th28;