co.combinatorics - Sperner's theorem and "pushing shadows around"

Let $mathcal{B}$ be a collection of $k$-sets , subsets of an $n$-set $S$. For $k < n$ define the shade of $mathcal{B}$ to be $$nabla mathcal{B}={ Dsubset S : |D|=k+1,exists Bin mathcal{B},Bsubset D}$$ and the shadow of $mathcal{B}$ to be
$$Delta mathcal{B}={ Dsubset S : |D|=k-1,exists Bin mathcal{B},Dsubset B}$$ Sperner proved the lemma: $|Delta mathcal{B}|geq frac{k}{n-k+1}|mathcal{B}|$ for $k > 0$, and $|nabla mathcal{B}|geq frac{n-k}{k+1}|mathcal{B}|$ for $k < n$.

This implies that if $kle frac{1}{2}(n-1)$, then $|nabla mathcal{B}|geq |mathcal{B}|$ and if $kgeqfrac{1}{2}(n+1)$ then $|Delta mathcal{B}|geq |mathcal{B}|$. Now the proof proceeds in the obvious steps: Suppose we have an antichain $mathcal{A}$, and it has $p_i$ elements of size $i$. If $i < frac{1}{2}(n-1)$ then from the above we can substitute them with $p_i$ elements of size $i+1$. Similarly for the elements of size $i > frac{1}{2}(n+1)$. You end up with an antichain of elements of size $lfloor frac{n}{2}rfloor$ giving you the proof of Sperner's theorem.

I really enjoyed Combinatorics of finite sets by I. Anderson which treats Sperner's theorem, LYM, Erdos-Ko-Rado, Kruskal-Katona etc. The above is just a sketch but there you can find all the details.