let n be Nat; :: thesis: support (pfexp n) c= SetPrimes
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (pfexp n) or x in SetPrimes )
assume x in support (pfexp n) ; :: thesis: x in SetPrimes
then x is Prime by NAT_3:34;
hence x in SetPrimes by NEWTON:def 6; :: thesis: verum