Top-bottom decisiveness lemma (source code)

= Top-bottom decisiveness lemma

For two agents and a <strategyproof> <social choice function>, if an alternative is selected when one agent ranks it first and the other ranks it last, it is selected whenever the first agent ranks it first, whatever the other agent reports. Changing the first agent's order preserves its attainable top choice; changing the second agent's order cannot offer it an improvement over a selected bottom alternative.