take n ; :: according to FINSEQ_1:def 13 :: thesis: PrimeDivisors n c= Seg n
thus PrimeDivisors n c= Seg n by NUMBER12:46; :: thesis: verum
thus verum ; :: thesis: verum