>>550
>ひとつ心配でもあるのは極限順序数の時
>K(λ)=∩K(μ)（μ<λ）にしているところだけど
順序数の個数のクラスの包含を考えて
（Ord⊃K(0)⊃K(1)⊃…⊃K(μ)⊃…⊃K(λ)）
共通部分を取る操作だけど
K(λ)::={κ::∀μ<λ:κ=k(μ)(κ)}
の定義に
k(μ)というクラス関数は登場するけど
クラスの量化子は使ってないから
クラス存在定理によって定義は可能と