let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in 6n+1_Primes or a in SetPrimes )
assume a in 6n+1_Primes ; :: thesis: a in SetPrimes
then ex k being Nat st
( a = (6 * k) + 1 & (6 * k) + 1 is prime ) ;
hence a in SetPrimes by NEWTON:def 6; :: thesis: verum