NatDivisors n c= Seg n by Th40;
hence NatDivisors n is included_in_Seg by FINSEQ_1:def 13; :: thesis: verum