theorem Th1: :: NAT_3:1
for a, b, c, d being Integer st a divides c & b divides d holds
a * b divides c * d