let n be Nat; :: thesis: ( ( n + 1 is prime implies primeNumbers (n,1) = {(n + 1)} ) & ( not n + 1 is prime implies primeNumbers (n,1) = {} ) )

hereby :: thesis: ( not n + 1 is prime implies primeNumbers (n,1) = {} )

assume A1: n + 1 is prime ; :: thesis: primeNumbers (n,1) = {(n + 1)}
n < n + 1 by NAT_1:13;
then A2: n + 1 in primeNumbers (n,1) by A1, Th74;
primeNumbers (n,1) c= {(n + 1)}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in primeNumbers (n,1) or y in {(n + 1)} )
assume A3: y in primeNumbers (n,1) ; :: thesis: y in {(n + 1)}
reconsider y = y as Nat by A3;
n < y by A3, Th74;
then ( n + 1 <= y & y <= n + 1 ) by A3, Th74, NAT_1:13;
then y = n + 1 by XXREAL_0:1;
hence y in {(n + 1)} by TARSKI:def 1; :: thesis: verum

end;

hence primeNumbers (n,1) = {(n + 1)} by A2, ZFMISC_1:33; :: thesis: verum

end;

assume A4: not n + 1 is prime ; :: thesis: primeNumbers (n,1) = {}
assume primeNumbers (n,1) <> {} ; :: thesis: contradiction
then consider y being object such that
A5: y in primeNumbers (n,1) by XBOOLE_0:def 1;
reconsider y = y as Nat by A5;
n < y by A5, Th74;
then ( n + 1 <= y & y <= n + 1 ) by A5, Th74, NAT_1:13;
then y = n + 1 by XXREAL_0:1;
hence contradiction by A4, A5, Th74; :: thesis: verum