Arrow の一般可能性定理

bewaadさんのとこ(http://bewaad.com/20050920.html#p01)で紹介されている面白い定理。自分なりに噛み砕いていうと、「個人の好みに基づいてグループ全体の好みを決定する合理的（推移的等の性質を満たす）な方法では、常にグループ全体の好みを決定しているかのように振る舞う個人が存在してしまう」という定理。この、全体の好みを決定している個人を「独裁者」と考えると、なかなか政治学的に刺激的な定理になる。興味深く読んでいたら、コメント欄でこの定理に関する証明がリンクされていた。
http://www.simplex.t.u-tokyo.ac.jp/~tomomi/text/Arrow8A.pdf
この証明自体はわかりやすかったんだが、bewaadさんのところで述べられている「パレート最適性」の条件がどこに含まれているのかよくわからなかった。あと、補題３が「全ての」場合についての証明になっているかどうかがよくわからない。あとでよく読もう。

（追記）元々のbewaadさんの記事からリンクされているモラルを科学する学問 | NetWindを読んでなかった。性質１がパレート最適性を表しているわけね。けど、パレート最適ってそういう定義だっけ？微妙に違和感が…