>>628
>ただφ自体は、選択公理という仮定によって誕生しているから
>これについては何の情報もない
から
>具体的にどんな順序かは全く不明(>>619)
が帰結される。

整列定理の証明は整列順序を構成はしているが、その構成に非構成的である選択関数を使っているから結局整列順序は非構成的。