theorem Th3: :: NTALGO_1:3

for i2, i1 being Integer st i2 <= 0 holds
i1 mod i2 <= 0