reconsider X = PrimeDivisors n as included_in_Seg Subset of SetPrimes by NUMBER12:45;
PrimeDivisorsFS n = Sgm X ;
hence ( PrimeDivisorsFS n is Chinese_Remainder & PrimeDivisorsFS n is positive-yielding ) ; :: thesis: verum