theorem :: NUMBER16:39

( ( for n being Nat st n > 1 holds
ex p being Prime st
( n < p & p < 2 * n ) ) iff for n being Nat st n > 1 holds
ex p being Prime st p |-count (n !) = 1 )