>>508
>>510-511の訳
Sの下界の一つをmとして、S’={|m|+x；x∈S} を考えれば、
これは自然数の部分集合になるので整列性が適用できる。

ただ、S’がNの部分集合になることとか、写像S→S’およびその
逆写像が順序を保存することとか、どう見ても自明っぽいことでも
厳密に書こうとすると意外と面倒なので、適当にガンガレ。