S と T を順序集合とし、f：S → T を残余(>>470) g を持つ写像とする。
>>473 より、任意の t ∈ T に対して f(x) ≦ t ⇔ x ≦ g(t)
即ち、x ∈ f^(-1)((-∞, t]) ⇔ x ∈ (-∞, g(t)]
よって、f^(-1)((-∞, t]) = (-∞, g(t)]
よって、g(t) は f^(-1)((-∞, t]) の最大元である。
よって、g は f により一意に定まる。