In this answer I sketch an easy proof of your lemma and then give some references. The easy proof uses Knaster's fixed point theorem: THEOREM. Let $S$ be any set (finite or infinite) and let $\varphi:\mathcal P(S)\to\mathcal P(S)$ be an order-preserving map, i.e., $X\subseteq Y\implies\varphi(X)\subseteq\varphi(Y).$ Then $\varphi$ has a fixed point. PROOF. Let $X_0=\bigcup\{X\in\mathcal P(S):X\subseteq\varphi(X)\}.$ It is easy to see that $\varphi(X_0)=X_0.$ (Knaster's fixed point theorem was set as a [Putnam Problem in 1957](https://mks.mff.cuni.cz/kalva/putnam/psoln/psol5712.html). The generalization to complete lattices is called the [Knaster-Tarski Theorem](http://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem).) Now let $B_1,B_2,G_1,G_2$ be the set of all first-class boys, second-class boys, first-class girls, and second-class girls, respectively; $B=B_1\cup B_2,\ G=G_1\cup G_2,\ B_1\cap B_2=G_1\cap G_2=\emptyset.$ By Hall's theorem there are matchings $f:B_1\to G$ and $g:G_1\to B.$ Define an order-preserving map $\varphi:\mathcal P(B_1)\to\mathcal P(B_1)$ by setting, for $X\subseteq B_1,$ $$\varphi(X)=B_1\setminus g[G_1\setminus f[X]].$$ By Knaster's fixed point theorem we have $\varphi(X_0)=X_0$ for some $X_0\subseteq B_1$. Now we can match the boys in $X_0$ with the girls in $f[X_0]$ and the girls in $G_1\setminus f[X_0]$ with the boys in $g[G_1\setminus f[X_0]].$ Here are some references related to your lemma: L. Mirsky, *Transversal Theory*, Academic Press, New York and London, 1971. L. Mirsky and Hazel Perfect, Systems of representatives, J. Math. Analysis Appl. 15 (1966), 520-568. O. Ore, *Theory of Graphs*, Amer. Math. Soc. Colloquium Publications No. 38, Providence, 1962 [Theorem 7.4.1]. Here is how your lemma is stated on p. 36 of Mirsky's book: > THEOREM 2.3.1. *Let $(X,\Delta,Y)$ be a deltoid and let $X',Y'$ be admissible subsets of $X,Y$ respectively. Then there exist linked sets $X_0,Y_0$ such that $X'\subseteq X_0\subseteq X,\ Y'\subseteq Y_0\subseteq Y.$* The jargon is defined on pp. 33-34. Namely, a *deltoid* $(X,\Delta,Y)$ is a bipartite graph with partite sets $X,Y$ and edge set $\Delta$; a set $X'\subseteq X$ is *admissible* if there is an injective matching of $X'$ to $Y$; a set $Y'\subseteq Y$ is *admissible* if there is an injective matching of $Y'$ to $X$; two sets $X_0\subseteq X,Y_0\subseteq Y$ are *linked* if there is a bijective matching of $X_0$ to $Y_0.$ **P.S.** Sergei Ivanov has commented that the result, as stated in the question, can be traced back to Dulmage & Mendelsohn, Some generalizations of the problem of distinct representatives, Canad. J. Math. 10 (1958) 230–241, Theorem 1.