theorem Th16: :: NAT_5:16

for n0, m0 being non zero Nat
for n1, m1 being Nat st n1 in NatDivisors n0 & m1 in NatDivisors m0 holds
n1 * m1 in NatDivisors (n0 * m0)