theorem Th6: :: EUCLIDLP:6

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