let n, k be Nat; :: thesis: ( k > 0 & n + 1 is prime & not (n + k) + 1 is prime implies card (primeNumbers ((n + 1),k)) = (card (primeNumbers (n,k))) - 1 )
assume that
A1: k > 0 and
A2: ( n + 1 is prime & not (n + k) + 1 is prime ) ; :: thesis: card (primeNumbers ((n + 1),k)) = (card (primeNumbers (n,k))) - 1
reconsider k1 = k - 1 as Nat by A1;
A3: card (primeNumbers ((n + 1),(k1 + 1))) = (card (primeNumbers ((n + 1),k1))) + (card (primeNumbers (((n + 1) + k1),1))) by Th79;
A4: card (primeNumbers (n,(1 + k1))) = (card (primeNumbers (n,1))) + (card (primeNumbers ((n + 1),k1))) by Th79;
( card (primeNumbers (n,1)) = 1 & card (primeNumbers (((n + 1) + k1),1)) = 0 ) by A2, Th81;
hence card (primeNumbers ((n + 1),k)) = (card (primeNumbers (n,k))) - 1 by A3, A4; :: thesis: verum