theorem Th9: :: EUCLIDLP:9

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