命題
X を束(過去スレ021の156)とする。
X の∨素元(>>157)全体を JP(X) とする。
>>177より x ∈ JP(X) のとき (↑x)^c ∈ Spec(X) (>>178) である。
写像 f:JP(X) → Spec(X) を f(x) = (↑x)^c により定義する。
このとき f は順序埋め込み(過去スレ021の227)である。

証明
x、y ∈ X、x ≦ y とする。
↑y ⊂ ↑x であるから、(↑x)^c ⊂ (↑y)^c である。

逆に、x、y ∈ X、(↑x)^c ⊂ (↑y)^c とする。
↑y ⊂ ↑x であるから y ∈ ↑x である。
よって、x ≦ y である。
証明終