thus card (primeNumbers (1,100)) = 26 by Th85; :: thesis: for n being Nat st n <> 1 holds
card (primeNumbers (n,100)) < 26
let n be Nat; :: thesis: ( n <> 1 implies card (primeNumbers (n,100)) < 26 )
assume A1: n <> 1 ; :: thesis: card (primeNumbers (n,100)) < 26
set S = card (primeNumbers (n,100));

per cases ( n <= 10 or n > 10 ) ;

suppose n <= 10 ; :: thesis: card (primeNumbers (n,100)) < 26

then not not n = 0 & ... & not n = 10 ;
then ( card (card (primeNumbers (n,100))) = 25 or card (card (primeNumbers (n,100))) < 25 ) by A1, Th85;
hence card (primeNumbers (n,100)) < 26 by XXREAL_0:2; :: thesis: verum

end;

suppose n > 10 ; :: thesis: card (primeNumbers (n,100)) < 26

then n >= 10 + 1 by NAT_1:13;
then card (card (primeNumbers (n,100))) <= 24 by Th96;
hence card (primeNumbers (n,100)) < 26 by XXREAL_0:2; :: thesis: verum

end;

end;