theorem Th80: :: NUMBER19:80

for n being Nat holds
( ( n + 1 is prime implies primeNumbers (n,1) = {(n + 1)} ) & ( not n + 1 is prime implies primeNumbers (n,1) = {} ) )