theorem :: ROBBINS2:39

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