for x being Real st x >= 2 holds
Product (Sgm { p where p is prime Element of NAT : p <= x } ) <= 4 to_power (x - 1)