now :: thesis: ex p being Nat st
( p is n _greater & p is prime )

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

A2: now :: thesis: for p being Prime holds p < n + 1

let p be Prime; :: thesis: p < n + 1
not p is n _greater by A1;
hence p < n + 1 by NAT_1:13; :: thesis: verum

end;

A3: now :: thesis: for p being set st p in SetPrimes holds
p in SetPrimenumber (n + 1)

let p be set ; :: thesis: ( p in SetPrimes implies p in SetPrimenumber (n + 1) )
assume A4: p in SetPrimes ; :: thesis: p in SetPrimenumber (n + 1)
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: verum

end;

now :: thesis: for p being set st p in SetPrimenumber (n + 1) holds
p in SetPrimes

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

end;

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

end;

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