theorem Th2: :: EUCLIDLP:2

for n being Nat
for x being Element of REAL n holds
( x - x = 0* n & x + (- x) = 0* n )