1 is not Prime by INT_2:def 4;
then A1: not 1 in SetPrimes by NEWTON:def 6;
2 in SetPrimes by NEWTON:def 6, INT_2:28;
hence SetPrimes 2 = {2} by ZFMISC_1:54, A1, FINSEQ_1:2; :: thesis: verum