theorem :: ROBBINS2:56

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