( not 0 + 1 is prime & not (0 + 21) + 1 is prime ) by XPRIMES0:22;
then A1: card (primeNumbers ((0 + 1),21)) = 8 by Lm5, Th82;
( 1 + 1 is prime & (1 + 21) + 1 is prime ) by XPRIMES1:2, XPRIMES1:23;
then A2: card (primeNumbers ((1 + 1),21)) = 8 by A1, Th82;
( 2 + 1 is prime & not (2 + 21) + 1 is prime ) by XPRIMES0:24, XPRIMES1:3;
then A3: card (primeNumbers ((2 + 1),21)) = 8 - 1 by A2, Th84;
A4: ( not 3 + 1 is prime & not (3 + 21) + 1 is prime ) by XPRIMES0:4, XPRIMES0:25;
A5: { n where n is Nat : card (primeNumbers (n,21)) = 8 } c= {0,1,2}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { n where n is Nat : card (primeNumbers (n,21)) = 8 } or x in {0,1,2} )
assume x in { n where n is Nat : card (primeNumbers (n,21)) = 8 } ; :: thesis: x in {0,1,2}
then consider n being Nat such that
A6: ( x = n & card (primeNumbers (n,21)) = 8 ) ;
( n < 5 & 5 = 4 + 1 ) by A6, Th98;
then n <= 4 by NAT_1:13;
then not not n = 0 & ... & not n = 4 ;
hence x in {0,1,2} by A6, A3, A4, Th82, ENUMSET1:def 1; :: thesis: verum

end;

{0,1,2} c= { n where n is Nat : card (primeNumbers (n,21)) = 8 }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {0,1,2} or x in { n where n is Nat : card (primeNumbers (n,21)) = 8 } )
assume x in {0,1,2} ; :: thesis: x in { n where n is Nat : card (primeNumbers (n,21)) = 8 }
then ( x = 0 or x = 1 or x = 2 ) by ENUMSET1:def 1;
hence x in { n where n is Nat : card (primeNumbers (n,21)) = 8 } by Lm5, A1, A2; :: thesis: verum

end;

hence { n where n is Nat : card (primeNumbers (n,21)) = 8 } = {0,1,2} by A5, XBOOLE_0:def 10; :: thesis: verum