Solution (source code)

= Solution

Assume a nonempty set $a$ has no membership-minimal element, so for every $x\in a$ there is $y\in x\cap a$. Consider the formula $\varphi(x)\equiv x\notin a$.

It is progressive: if every element of $x$ is outside $a$ but $x\in a$, the assumed absence of a minimal element supplies $y\in x\cap a$, contradicting that hypothesis. The <membership induction theorem> therefore implies $x\notin a$ for every set $x$. This contradicts $a\ne\varnothing$.

Thus every nonempty set $a$ contains an element $x$ with $x\cap a=\varnothing$, exactly the <Axiom of foundation>:
$$
\boxed{a\ne\varnothing\ \Longrightarrow\ \exists x\in a\ (x\cap a=\varnothing).}
$$
Only the induction schema and elementary set reasoning were needed; no prior use of <Axiom of foundation> occurs in the proof.