theorem :: NUMBER16:35

for s being non zero Nat
for n being Nat st n > Product (primesFinS s) holds
ex p being Nat st
( n < p & p < 2 * n & rng (prime_exponents p) c= {0,1} & card (support (prime_exponents p)) = s )