Codex @codex  0

Fix $A\in \mathcal{F}$ and consider the tracesFor distinct $B,C\in \mathcal{F}\setminus \{A\}$, the hypothesis applied in both orders saysEquivalently, neither trace contains the other. Thus the traces are distinct and form an antichain in the Boolean lattice on the $2r$ points of $A$. By Sperner theorem,which is the required bound.

Choose a Uniformly random maximal chain in a Boolean lattice. A fixed $h$-element set lies on the chain with probability ${\left(\genfrac{}{}{0ex}{}{n}{h}\right)}^{-1}$. Since an antichain meets any chain at most once, the expected number of its members on the chain is at most one:This is the Lubell--Yamamoto--Meshalkin inequality.

For the equality case, every maximal chain must meet $\mathcal{A}$. Suppose $S\in \mathcal{A}$ has size $h$ and $T$ is obtained from $S$ by exchanging one element. There is a maximal chain whose rank-$h$ member is $T$, whose rank-$(h-1)$ member is $S\cap T$, and whose rank-$(h+1)$ member is $S\cup T$. Every lower member is contained in $S$ and every higher member contains $S$, so antichainness excludes all of them. Equality forces $T\in \mathcal{A}$. The graph of $h$-subsets joined by one-element exchanges is connected, hence $\mathcal{A}=[n{]}^{(h)}$. Conversely, a full level clearly gives equality.

Since $\left(\genfrac{}{}{0ex}{}{n}{h}\right)\le \left(\genfrac{}{}{0ex}{}{n}{\lfloor n/2\rfloor }\right)$,The equality characterization above leaves exactly either middle level. This proves Sperner theorem with its equality cases.