assume {} in 6n+1_Primes ; :: according to SETFAM_1:def 8 :: thesis: contradiction
then ex k being Nat st
( 0 = (6 * k) + 1 & (6 * k) + 1 is prime ) ;
hence contradiction ; :: thesis: verum