theorem :: MOEBIUS2:2

for n being Nat holds support (pfexp n) c= SetPrimes