assume A1: for p being natural number holds
( not p is n _greater or not p is prime ) ; :: thesis:

A2: now :: thesis:

let p be natural prime number ; :: thesis:
not p is n _greater by A1;
hence p < n + 1 by NAT_1:13; :: thesis:

end;

A3: now :: thesis:

let p be set ; :: thesis:
assume A4: p in SetPrimes ; :: thesis:
then reconsider p1 = p as Element of NAT ;
A5: p1 is prime by A4, NEWTON:def 6;
then p1 < n + 1 by A2;
hence p in SetPrimenumber (n + 1) by A5, NEWTON:def 7; :: thesis:

end;

let p be set ; :: thesis:
assume A6: p in SetPrimenumber (n + 1) ; :: thesis:
reconsider n1 = n + 1 as Nat ;
SetPrimenumber n1 c= SetPrimes by NEWTON:68;
hence p in SetPrimes by A6; :: thesis:

end;

then SetPrimes = SetPrimenumber (n + 1) by A3;
hence contradiction ; :: thesis:

end;

hence ex b₁ being natural number st
( b₁ is n _greater & b₁ is prime ) ; :: thesis: