theorem Th40: :: MOEBIUS1:40

for n being non zero Nat holds NatDivisors n c= Seg n