theorem Th2: :: JORDAN4:2

for i, j being Nat st j <= i & i < j + j holds
( i mod j = i - j & i mod j = i -' j )