The Souslin operation

Work in ZF. For a set $X$ and a scheme $(A_s{)}_{s\in {\mathbb{N}}^{<\omega }}$ of subsets of $X$, with finite prefixes as in Trees and their bodies and branches in Baire sequence space ${\mathbb{N}}^{\mathbb{N}}$ and its cylinder topology, the Souslin operation is

$\mathsf{S}(A)={\bigcup }_{f\in {\mathbb{N}}^{\mathbb{N}}}{\bigcap }_{n\in \mathbb{N}}{A}_{f\upharpoonright n}\mathrm{.}$

The intersection includes $n=0$, so $\mathsf{S}(A)\subseteq A_{\mathrm{\varnothing }}$. Setting $A_{\mathrm{\varnothing }}=X$ makes that term neutral; setting it empty makes the result empty. All unions and intersections are indexed by sets, so Separation and Union define a subset of $X$.

One may normalize to a decreasing scheme by putting $B_s={\bigcap }_{t\subseteq s}{A}_t$, where prefixes include $s$ itself. If $s\subseteq u$, its prefix family is included in that of $u$, so $B_u\subseteq B_s$. For each fixed branch $f$, membership in every $B_{f\upharpoonright n}$ implies membership in $A_{f\upharpoonright n}$ by taking that prefix itself. Conversely membership in all $A_{f\upharpoonright j}$ implies membership in every $B_{f\upharpoonright n}$, since each prefix of $f\upharpoonright n$ is $f\upharpoonright j$ for some $j\le n$. The branch intersections, and hence the two Souslin results, are equal. This also covers the empty ambient set and uses no choice.