>>767
>G の任意の x, y に対して inf(y - x, 0) が存在するとする。

G の元 x, y に対して inf(y - x, 0) が存在するとする。