( not 0 + 1 is prime & (0 + 100) + 1 is prime )
by XPRIMES1:101;
then A1:
( card (primeNumbers ((0 + 1),100)) = 25 + 1 & 25 + 1 = 26 )
by Lm5, Th83;
( 1 + 1 is prime & not (1 + 100) + 1 is prime )
by XPRIMES0:102, XPRIMES1:2;
then A2:
( card (primeNumbers ((1 + 1),100)) = 26 - 1 & 26 - 1 = 25 )
by A1, Th84;
A3:
( 2 + 1 is prime & (2 + 100) + 1 is prime )
by XPRIMES1:3, XPRIMES1:103;
then A4:
card (primeNumbers ((2 + 1),100)) = 25
by A2, Th82;
A5:
( not 3 + 1 is prime & not (3 + 100) + 1 is prime )
by XPRIMES0:4, XPRIMES0:104;
then A6:
card (primeNumbers ((3 + 1),100)) = 25
by A4, Th82;
( 4 + 1 is prime & not (4 + 100) + 1 is prime )
by XPRIMES0:105, XPRIMES1:5;
then A7:
( card (primeNumbers ((4 + 1),100)) = 25 - 1 & 25 - 1 = 24 )
by A6, Th84;
( not 5 + 1 is prime & not (5 + 100) + 1 is prime )
by XPRIMES0:6, XPRIMES0:106;
then A8:
card (primeNumbers ((5 + 1),100)) = 24
by A7, Th82;
( 6 + 1 is prime & (6 + 100) + 1 is prime )
by XPRIMES1:7, XPRIMES1:107;
then A9:
card (primeNumbers ((6 + 1),100)) = 24
by A8, Th82;
( not 7 + 1 is prime & not (7 + 100) + 1 is prime )
by XPRIMES0:8, XPRIMES0:108;
then A10:
card (primeNumbers ((7 + 1),100)) = 24
by A9, Th82;
( not 8 + 1 is prime & (8 + 100) + 1 is prime )
by XPRIMES0:9, XPRIMES1:109;
then A11:
card (primeNumbers ((8 + 1),100)) = 24 + 1
by A10, Th83;
( not 9 + 1 is prime & not (9 + 100) + 1 is prime )
by XPRIMES0:10, XPRIMES0:110;
hence
( card (primeNumbers (1,100)) = 26 & ( for k being Nat st ( k = 0 or k = 2 or k = 3 or k = 4 or k = 9 or k = 10 ) holds
card (primeNumbers (k,100)) = 25 ) & ( for k being Nat st ( k = 5 or k = 6 or k = 7 or k = 8 ) holds
card (primeNumbers (k,100)) < 25 ) )
by Lm5, A1, A3, A5, A4, A7, A8, A9, A10, A11, Th82; verum