Let $q' = p(α, q, k)$ be given by $GaifmanLocality$. A formula of rank at most $q$ uses finitely many relation symbols. Over the sublanguage of these symbols it is equivalent, on finite structures, to a Boolean combination of basic $7^q$-local sentences and $7^q$-local formulas of rank at most $q'$. The sentences have the same truth value for both tuples. A local formula holds of a tuple in the structure if and only if it holds in the induced substructure, by $LocalSubstructure$, since the balls of the sublanguage are contained in those of $L$. In the induced substructures, the two tuples satisfy the same formulas of rank at most $q'$.