Web 部室、読んでると前向きな気持ちになれないので退部

実数の全順序性 (x < y || x = y || x > y) って排中律が無いと言えないというのは知らなかった。閉区間上の連続関数が最大値を持つというのも排中律が無いと言えないらしい。実数の当たり前と思ってる性質が結構排中律に依存しているらしい。