 Downward closure of a set family

For a set family $\mathcal{A}\subseteq \mathcal{P}([n])$, its downward closure is $\downarrow \mathcal{A}=\{S:\text{some }A\in \mathcal{A}\text{ has }S\subseteq A\}$. It is the smallest down-set containing $\mathcal{A}$, just as the upward closure of a set family is the smallest up-set containing it. The two closures allow Harris' inequality to control sizes of a cross-Sperner family pair.