theorem Th9: :: NAT_D:9

for h, i, j being natural Number st i divides j holds
i divides j * h by INT_2:2;