theorem Th4: :: EUCLIDLP:4

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