let n be Nat; :: thesis: card (primeNumbers (n,4)) = (((card (primeNumbers (n,1))) + (card (primeNumbers ((n + 1),1)))) + (card (primeNumbers ((n + 2),1)))) + (card (primeNumbers ((n + 3),1)))
A1: card (primeNumbers (((n + 1) + 1),(1 + 1))) = (card (primeNumbers (((n + 1) + 1),1))) + (card (primeNumbers ((((n + 1) + 1) + 1),1))) by Th79;
A2: card (primeNumbers ((n + 1),(2 + 1))) = (card (primeNumbers ((n + 1),1))) + (card (primeNumbers (((n + 1) + 1),2))) by Th79;
card (primeNumbers (n,(3 + 1))) = (card (primeNumbers (n,1))) + (card (primeNumbers ((n + 1),3))) by Th79;
hence card (primeNumbers (n,4)) = (((card (primeNumbers (n,1))) + (card (primeNumbers ((n + 1),1)))) + (card (primeNumbers ((n + 2),1)))) + (card (primeNumbers ((n + 3),1))) by A1, A2; :: thesis: verum