Sorry, that should be:<p><pre><code>    ∃ epsilon ∈ [SUBSET S → S] : ∀x ∈ SUBSET S : x ≠ {} ⇒ epsilon[x] ∈ x
</code></pre>
As a matter of fact, TLA+ also allows unbounded quantifications, so you could write:<p><pre><code>    ∃ epsilon : ∀x : x ≠ {} ⇒ epsilon[x] ∈ x
</code></pre>
However, this form is rarely used because TLC, (TLA+&#x27;s model checker, which only supports a subset of TLA+), doesn&#x27;t support unbounded quantifiers, and they are not necessary when modeling real programs. I&#x27;m not sure about TLAPS (the proof assistant), but I believe it handles it fine.