let n be non zero Nat; :: thesis: 5 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 5 <= (6 * n) + 1 by XXREAL_0:2;
then A1: 5 in <=6n+1 n ;
5 in SetPrimes by XPRIMES1:5, NEWTON:def 6;
hence 5 in (<=6n+1 n) /\ SetPrimes by A1, XBOOLE_0:def 4; :: thesis: verum