theorem :: NUMBER19:99
( card (primeNumbers (1,100)) = 26 & ( for n being Nat st n <> 1 holds
card (primeNumbers (n,100)) < 26 ) )