これは面白いの。√2^√2を考えるわ。もしこれが有理数であるなら、無理数の無理数乗が有理数ということになるわね。
じゃあ、もし√2^√2が有理数でない、つまり無理数なら、(√2^√2)^√2を考えるの。すると
(√2^√2)^√2 = √2^(√2 x √2) = √2^2 = 2
となってやはり無理数の無理数乗が有理数になるわ。
√2^√2は有理数であるか有理数でないかのどちらかであり、どっちにしても無理数の無理数乗が有理数になることがあることがわかったから、これで証明できたわ。
この「√2^√2は有理数であるか有理数でないかのどちらかである」を真としているのが排中律を使っている部分よ。
ちなみに構成的証明は √2^{log_2 9} = 3 というもので、>>41の(1)の方法はこれをアレンジしたの。