theorem Th12: :: INT_4:12

for i being Integer holds 0 = 0 mod i