let n be non zero Nat; :: thesis: 7 in (<=6n+1 n) /\ SetPrimes
0 + 1 <= n by NAT_1:13;
then 6 * 1 <= 6 * n by XREAL_1:64;
then 6 + 1 <= (6 * n) + 1 by XREAL_1:6;
then A1: 7 in <=6n+1 n ;
7 in SetPrimes by XPRIMES1:7, NEWTON:def 6;
hence 7 in (<=6n+1 n) /\ SetPrimes by A1, XBOOLE_0:def 4; :: thesis: verum