>>171の別証明(本質的には同じだが)

命題
X を空でない有限分配束(過去スレ021の322)とする。
B を X の∨既約元(過去スレ021の403)全体とする。
|B| = length(X) (過去スレ021の379)である。
ここで、|B| は B の元の個数である。

証明
n = length(X) とする。
0 = x_0 ＜ x_1 ＜ ．．．＜ x_n = 1 を X における長さ n の鎖 C とする。
>>168より、φ = B↓(x_0) ⊂ B↓(x_1) ⊂ ．．．⊂ B↓(x_n) = B は
Down(B) における極大鎖である。
各 i、i = 0、．．．、n-1 に対して
|B↓(x_(i+1)) - B↓(x_i)| = 1 であることを証明しよう。
x = x_i、y = x_(i+1) とおく。
a、b ∈ B↓(y) - B↓(x) とする。
a∨x = b∨x = y
よって、a = a∧(a∨x) = a∧(b∨x) = (a∧b)∨(a∧x)
a は∨既約だから a = a∧b または a = a∧x
よって、a ≦ b または a ≦ x
しかし、a ≦ x では有り得ないから a ≦ b である。
同様に b ≦ a である。
よって、a = b である。
よって、|B↓(x_i)| = i、i = 0、．．．、n である。
よって、|B| = |B↓(x_n)| = n である。
証明終