Let HF be the collection of the hereditarily finite well-founded sets and let the primitive language of set theory be the first-order language which contains binary symbols for equality and membership only. As announced in a previous paper by the authors, "Truth in V for ∃*∀∀-sentences is decidable," truth in HF for ∃*∀∀-sentences of the primitive language is decidable. The paper provides the proof of that claim.