🚀 go-pugleaf

I've heard this result but can't recall where. Can anyone provide a
reference or related results for other number pairs?

Theorem: Suppose that there is a choice function for 2 element sets
, then there is a choice function for 4 element sets.

Proof: Given a set {a,b,c,d} form each of the 6 2-element subsets
and apply the choice function to it. Each of the four elements is
chosen 0,1,2 or 3 times. If any is chosen 3 times, choose it (it must
be unique). If none is chosen 3 times and one is never chosen, choose
it (IT must be unique. The remaining possibility is that two are chosen 
twice and 2 chosen once. Take the two chosen once (or twice, just decide 
which) and let the chosen element be that chosen by the function for 
that pair/////

So this result might be termed AC2 implies AC4. 
Thanks,
Aaron Meyerowitz