theorem Th1: :: NUMBER19:1

for n, m being Nat st n divides m holds
NatDivisors n c= NatDivisors m