theorem Th1: :: JORDAN4:1

for i, j being Nat st j < i & i < j + j holds
i mod j <> 0