theorem Th4: :: EUCLID_7:5

for n being Nat
for a, b, c being Element of REAL n holds ((a - b) + c) + b = a + c