If a formula $φ(x, y)$ has the independence property on $C$, then for a graph $H$ on $m$ vertices take the elements $a₀, …, a_{m-1}$ and color the set $A$ of them and the set $B$ of the elements $b_{ij}$ for the edges $ij$ of $H$. Two distinct elements of $A$ are adjacent in $H$ if and only if they have a common $φ$-neighbor in $B$. So $C$ transduces all graphs. Conversely, a transduction of all graphs produces the incidence graph between ${0, …, m-1}$ and its subsets, so its edge formula has the independence property.

The argument is carried out for the graph classes of the archive and mathlib formulas, and transferred to the graph classes used here and the translation of formulas.