But upsetting the constructivists is the whole point! (That is: what's so cute about that proof is that it tells you that there's a solution to irrational^irrat

But upsetting the constructivists is the whole point! (That is: what's so cute about that proof is that it tells you that there's a solution to irrational^irrational=rational, and that it's one of two things, but it doesn't tell you which. Also, I think it's a little shorter and more elegant than using sqrt(10)^log10(4). Don't you?)