theorem Th2: :: JORDAN5D:2

for i being Nat st 3 <= i holds
i mod (i -' 1) = 1