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

hereby :: thesis: ( not n + 1 is prime implies card (primeNumbers (n,1)) = 0 )

assume n + 1 is prime ; :: thesis: card (primeNumbers (n,1)) = 1
then primeNumbers (n,1) = {(n + 1)} by Th80;
hence card (primeNumbers (n,1)) = 1 by CARD_1:30; :: thesis: verum

end;

assume not n + 1 is prime ; :: thesis: card (primeNumbers (n,1)) = 0
then primeNumbers (n,1) = {} by Th80;
hence card (primeNumbers (n,1)) = 0 ; :: thesis: verum