theorem Th1: :: NAT_3:1

for a, b, c, d being Nat st a divides c & b divides d holds
a * b divides c * d