theorem :: ROBBINS2:33

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