命題
X を前順序集合(過去スレ008の139)とし、f:X → X を閉包作用子(>>632)とする。
f に関する閉元(>>650)全体 F はX の飽満(>>669)な閉包系(>>668)である。

証明
x ∈ F、x 〜 y (>>567)とする。
y 〜 x 〜 f(x) 〜 f(y) より、y 〜 f(y)
よって、y ∈ F
よって、F は飽満である。

x ∈ X に対して x ≦ y、y ∈ F とする。
f(x) ≦ f(y) 〜 y
よって、f(x) ≦ y
よって、f(x) は [x, +∞) ∩ F の最小元である。
よって、F は X の閉包系である。
証明終