p in SetPrimes by NEWTON:def 6;
hence In (p,SetPrimes) = p by SUBSET_1:def 8; :: thesis: verum