The Souslin operation preserves the Baire property

Given E, let U be the union of those basis opens V for which $E\cap V$ is meagre. Countability of the basis and F1 with A1 make $E\cap U$ meagre. Put $F=X\setminus U$ and $H=E\cup F$. H differs from closed F by $E\cap U$, so is Baire-property by F1. Suppose a Baire-property D contains E. Then $C=H\setminus D$ is Baire-property by F1, disjoint from E and contained in F. If C were nonmeagre, choose open O with $C\mathrm{△}O$ meagre. O is nonmeagre, for otherwise so would C be by the ideal property. Since $O\setminus C$ is meagre and C misses E, $E\cap O$ is meagre. Every basis open inside O then belongs to the union defining U; hence $O\subseteq U$ and $O\cap C=\mathrm{\varnothing }$. This makes $O=O\setminus C$ meagre, a contradiction. Thus $H\setminus D$ is meagre as required.

For a Baire-property scheme normalize it by F2 to a decreasing scheme $(A_s)$, using F1 for finite intersections. Let $E_s={\bigcup }_{f\supseteq s}{\bigcap }_n{A}_{f\upharpoonright n}$. Then $E_s\subseteq A_s$ and $E_s={\bigcup }_k{E}_{s^{⌢}k}$. By step 1.1 and A1 choose Baire-property envelopes H_s of E_s (a countable family of nonempty sets of subset witnesses). Define $B_s=A_s\cap {\bigcap }_{t\subseteq s}{H}_t$. These are Baire-property and decrease along extensions. Also $E_s\subseteq B_s$, because $E_s\subseteq E_t\subseteq H_t$ for every prefix t. As $B_s\subseteq H_s$, it remains an envelope of E_s.

The union ${\bigcup }_k{B}_{s^{⌢}k}$ is a Baire-property superset of E_s. Therefore the envelope property makes $C_s=B_s\setminus {\bigcup }_k{B}_{s^{⌢}k}$ meagre. The union C of C_s over all finite words is meagre by F1 and A1. For $x\in B_{\mathrm{\varnothing }}\setminus C$, whenever $x\in B_s$ there is a child with x in its B-set, since $x\mathrm{\notin }{C}_s$. Recursively choose the least such child index. This defines a branch f with $x\in B_{f\upharpoonright n}\subseteq A_{f\upharpoonright n}$ for every n, and hence $x\in \mathsf{S}(A)$ by F2. Conversely $\mathsf{S}(A)=E_{\mathrm{\varnothing }}\subseteq B_{\mathrm{\varnothing }}$. Thus the Baire-property set $B_{\mathrm{\varnothing }}$ differs from $\mathsf{S}(A)$ by a subset of meagre C, so F1 proves the latter Baire-property.

For a Polish X, dense metric centres and positive rational radii give a countable basis. F3 with A1 represents every analytic set by a closed scheme. Its entries are Baire-property by F1; step 3.1 applies to prove the analytic assertion. Empty entries, including an empty root, require no alteration of the envelope argument. QED.