theorem :: ROBBINS2:29

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