PrimeDivisors n c= Seg n by NUMBER12:46;
hence PrimeDivisors n is finite ; :: thesis: verum