let n be Nat; :: thesis: for p being Prime st p < primenumber (n + 1) holds
p <= primenumber n
let p be Prime; :: thesis: ( p < primenumber (n + 1) implies p <= primenumber n )
assume A1: p < primenumber (n + 1) ; :: thesis: p <= primenumber n
set q1 = primenumber n;
set q2 = primenumber (n + 1);
(card (SetPrimenumber p)) + 1 <= card (SetPrimenumber (primenumber (n + 1))) by A1, CardSetPrime1;
then (card (SetPrimenumber p)) + 1 <= n + 1 by NEWTON:def 8;
then A2: card (SetPrimenumber p) <= n by XREAL_1:6;
assume primenumber n < p ; :: thesis: contradiction
then (card (SetPrimenumber (primenumber n))) + 1 <= card (SetPrimenumber p) by CardSetPrime1;
then n + 1 <= card (SetPrimenumber p) by NEWTON:def 8;
then n + 1 <= n by A2, XXREAL_0:2;
hence contradiction by XREAL_1:29; :: thesis: verum