theorem Th3: :: JORDAN4:3

for i, j being Nat holds (j + j) mod j = 0