Gives conditions for when a part of a bipartite graph has a matching. For a bipartite graph G with parts A and B, there is a matching for every element of A if and only if for every W ⊆ A it is the case that |W|≤|NG(W)|, where NG(W) denotes the neighbourhood of W.