theorem Th8: :: EUCLIDLP:8

for n being Nat
for x1, x2, x3 being Element of REAL n holds - ((x1 + x2) + x3) = ((- x1) + (- x2)) + (- x3)