補題
G を可換束群(過去スレ009の761)とする。
(x_i), i ∈ I を G の元の族で x = sup {x_i; i ∈ I} が存在するとする。
このとき inf(x, 0) = sup {inf(x_i, 0) ; i ∈ I} である。

証明
任意の i ∈ I に対して x_i ≦ x であるから
inf(x_i, 0) ≦ inf(x, 0) である。

逆に、任意の i ∈ I に対して inf(x_i, 0) ≦ a とする。
x_i = sup(x_i, 0) + inf(x_i, 0) であるから
x_i ≦ sup(x_i, 0) + a ≦ sup(x, 0) + a
よって、x ≦ sup(x, 0) + a
即ち、x - sup(x, 0) ≦ a
左辺は inf(x, 0) であるから、inf(x, 0) ≦ a
証明終