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∃ f c,2  f.Monic ∧3    f.natDegree = 4 ∧4      (f.rootSet ℂ).ncard = 4 ∧5        0 < c ∧6          (Erdos1047.componentsIn (Erdos1047.sublevelSet f c)).ncard = 4 ∧7            ∃ t ∈ Erdos1047.componentsIn (Erdos1047.sublevelSet f c), ¬Convex ℝ t