theorem :: NUMBER16:40

( ( for n being Nat st n > 5 holds
ex p, q being Prime st
( n < p & p < q & q < 2 * n ) ) implies for n being Nat st n > 10 holds
ex p, q being Prime st
( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 ) )