Equivalent Sperner-family formulation of the s-extremal extension conjecture

Let $[n]=\{1,\ldots,n\}$, let $\mathcal{S}\subseteq 2^{[n]}$ be a Sperner family, meaning that no member of $\mathcal{S}$ contains another, and let $h:\mathcal{S}\to 2^{[n]}$ satisfy $h(S)\subseteq S$ for every $S\in\mathcal{S}$. For $S\in\mathcal{S}$ and $A\subseteq S$, let $\mathcal{Q}_{S,A}$ denote the associated family used in the paper. Equivalent form of the s-extremal extension conjecture. There exists $S_0\in\mathcal{S}$ such that

$$\mathcal{Q}_{S_0,h(S_0)}\not\subseteq\bigcup_{S\in\mathcal{S}\setminus\{S_0\}}\mathcal{Q}_{S,h(S)}.$$

This is stated as an equivalent formulation of the main extension conjecture and is proved in the paper for Sperner families of size at most four; the general conjecture remains open.