Let $f\in \mathbb{C}[x]$ be a monic polynomial with $m$ distinct roots, and let $c>0$ be a constant small enough such that $\{ z: \lvert f(z)\rvert\leq c\}$ has $m$ distinct connected components.

1(Erdos1047.componentsIn2        (Erdos1047.strictSublevelSet (Polynomial.X * (Polynomial.X ^ 5 - 1)) (5 * 6 ^ (-6 / 5)))).ncard =3    6 ∧4  ∃ t ∈ Erdos1047.componentsIn (Erdos1047.strictSublevelSet (Polynomial.X * (Polynomial.X ^ 5 - 1)) (5 * 6 ^ (-6 / 5))),5    ¬Convex ℝ t