theorem Th82: :: POLYNOM9:82

ex Z being INT -valued Polynomial of 17,F_Real st
( vars Z c= {0} \/ (17 \ 8) & ( for xk being Nat st xk > 0 holds
( xk + 1 is prime iff ex x being INT -valued Function of 17,F_Real st
( x /. 8 = xk & x /. 9 is positive Nat & x /. 10 is positive Nat & x /. 11 is positive Nat & x /. 12 is positive Nat & x /. 13 is positive Nat & x /. 14 is Nat & x /. 15 is Nat & x /. 16 is Nat & x /. 0 is Nat & eval (Z,x) = 0. F_Real ) ) ) )