theorem ThDivs: :: NUMBER18:12

for n being non zero Nat holds #divs n = card (NatDivisors n)