theorem :: ROBBINS2:57

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