FinDLat を有限分配束(過去スレ021の322)とその間の{0, 1}-準同型(>>214)全体のなす圏とする。
FinPoset を有限順序集合とその間の単調増加写像全体のなす圏とする。

f：X → Y を FinDLat における射とする。
>>216より、写像 f^(-1)：Spec(Y) → Spec(X) が得られる。
f^(-1) は明らかに FinPoset における射である。
よって、関手 Spec：FinDLat → (FinPoset)^o が得られる。
ここで、(FinPoset)^o はFinPosetの双対圏(過去スレ017の352)である。

逆に g：S → T を FinPoset における射とする。
過去スレ021の589より 写像 g^(-1)：Down(T) → Down(S) (過去スレ021の516)が得られる。
g^(-1) は明らかに FinDLat における射である。
よって、関手 Down：(FinPoset)^o → FinDLat が得られる。

>>202より合成関手 Down・Spec は単位関手 1_FinDLat に自然同型(過去スレ018の144)である。
>>213より合成関手 Spec・Down は単位関手 1_(FinPoset)^o に自然同型である。
よって、FinDLat と (FinPoset)^o は圏同値(過去スレ017の404)である。