for n being Element of NAT holds Product (Sgm { p where p is prime Element of NAT : p <= n + 1 } ) <= 4 to_power n