Hall's marriage theorem for a finite bipartite graph

For $\mathrm{\mid }X\mathrm{\mid }=0$ the empty matching saturates $X$; for $\mathrm{\mid }X\mathrm{\mid }=1$, Hall gives a neighbour and its incident edge saturates $X$.

Any matching that saturates $X$ assigns distinct neighbours to each $S\subseteq X$, hence has $\mathrm{\mid }N(S)\mathrm{\mid }\ge \mathrm{\mid }S\mathrm{\mid }$.

In the strict case with $\mathrm{\mid }X\mathrm{\mid }\ge 2$, choose any edge $xy$; [L1] gives Hall after deleting $x,y$, so induction supplies a matching there saturating $X\setminus \{x\}$, and adjoining $xy$ saturates $X$.

In the tight case, [L1] gives Hall on the two smaller left parts $S$ and $X\setminus S$; induction gives saturating matchings in each, and their disjoint vertex sets let their union saturate $X$.

The base cases and the two alternatives prove Hall's sufficient direction by [L2], and step 1.2 proves its necessary direction.