命題
X を分配束(過去スレ021の322)とする。
length(X) (過去スレ021の379)が有限なら X は有限集合である。

証明
X は空でないと仮定してよい。
B を X の∨既約元(過去スレ021の403)全体とする。
X は極小条件(過去スレ021の397)を満たすから
過去スレ021の416より、X の最小限でない任意の元は有限個の∨既約元の結びとなる。
よって、B が有限集合であることを示せばよい。
n = length(X) とする。
0 = x_0 ＜ x_1 ＜ ．．．＜ x_n = 1 を X における長さ n の鎖 C とする。
X は極小条件(過去スレ021の397)を満たすから>>167より
B-下写像(過去スレ021の297) B↓：X → Down(B) は束埋め込み(>>166)である。
よって、φ = B↓(x_0) ⊂ B↓(x_1) ⊂ ．．．⊂ B↓(x_n) = B は
Down(B) における鎖(過去スレ021の377)である。
>>173の証明と同様にして各 i、i = 0、．．．、n-1 に対して
|B↓(x_(i+1)) - B↓(x_i)| = 1 である。
よって、|B↓(x_i)| = i、i = 0、．．．、n である。
よって、|B| = |B↓(x_n)| = n である。
証明終