let n be non zero Nat; :: thesis: (primenumber (1 + (primeindex (LP<=6n+1 n)))) - (LP<=6n+1 n) >= 4
set LP = LP<=6n+1 n;
set s = primenumber (1 + (primeindex (LP<=6n+1 n)));
set r = LP<=6n+1 n;
LP<=6n+1 n in (<=6n+1 n) /\ SetPrimes by XXREAL_2:def 8;
then LP<=6n+1 n in <=6n+1 n by XBOOLE_0:def 4;
then A1: LP<=6n+1 n <= (6 * n) + 1 by Th7;
primenumber (1 + (primeindex (LP<=6n+1 n))) >= (6 * n) + 5 by Th29;
then (primenumber (1 + (primeindex (LP<=6n+1 n)))) - (LP<=6n+1 n) >= ((6 * n) + 5) - ((6 * n) + 1) by A1, XREAL_1:13;
hence (primenumber (1 + (primeindex (LP<=6n+1 n)))) - (LP<=6n+1 n) >= 4 ; :: thesis: verum