for n being Element of NAT st n >= 1 holds
ex p being Prime st
( n < p & p <= 2 * n )