---
title: "有界子集落在受控层"
module: L.GCH.BoundedSubset
lang: zh
site: "Bedrock"
description: "有界子集在受控层出现"
stage: "证明 GCH"
reading_order: 119
canonical: https://bedrock.institute/zh/L.GCH.BoundedSubset.html
html: L.GCH.BoundedSubset.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/BoundedSubset.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Axioms.Numerals, L.Stage, L.Cardinal, L.GCH.Assembly, L.InjectionComposition, L.GCH.SkolemHull, L.GCH.CardinalSquareLaw, L.GCH.AdequateStages, L.GCH.StageCountingTools, L.GCH.StageInjection, L.GCH.OmegaRecursion, L.GCH.HullCounting]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.BoundedSubset.md, https://bedrock.institute/ja/L.GCH.BoundedSubset.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 有界子集落在受控层

有界子集定理从如下数据出发：内部基数 `κ` 的底层集合是序数且不属于 `ω`，任意可构造集合 `y` 的每个外围成员都属于 `κ`。定理在命题截断下给出可构造序数 `β`，使 `y ∈ Lset β`，并存在编码单射 `β ↪ κ`。这里不假设 `y` 由某个公式定义，不选取最小层，也不随 `y` 统一选取 `β`。

```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```

本证明的经典性只来自这里显式给出的排中律实例。该假设支撑本章所用的层、壳与编码映射等先前构造；它不会把最终的截断存在变成一族已选定的见证。

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

固定宇宙层级 `ℓ`，并假设层级 `ℓ-suc ℓ` 上的排中律。下文全部构造，包括最终的有界子集定理，都只依赖这一项经典假设，而不依赖任何选择原理。

```agda
module L.GCH.BoundedSubset {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

整个论证必须始终区分两类对象。`κ`、`α₀`、`lam` 以及后文的 `β` 等符号表示外围累积层级中的集合，其中一些会被证明为序数；`Lset κ`、`Lset α₀`、`Lset lam` 与 `Lset β` 则表示相应的可构造层。属于层索引与属于该索引所确定的层是两个不同的断言。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( #∈ω )
```

第一项任务是把 `κ` 与 `y` 一同放进某个足够高的可构造层。由于 `y` 已作为可构造集合给出，可以直接取得它的某个出现层；这一构造不使用定义 `y` 的公式，也不使用任何有限的定义参数表。

```agda
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Numerals {ℓ} using ( pairʟ )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL )
```

核心策略是把单点 `y` 添入 `Lset κ`，从这个传递起始集生成初等 Skolem 壳，再应用凝聚。先用 `κ` 计数起始集，便可进一步用 `κ` 计数整个壳；凝聚随后把塌缩后的壳识别为某个层 `Lset β`。

```agda
open import L.GCH.Assembly {ℓ} lem using ( InternalBoundedSubset )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.GCH.SkolemHull {ℓ} lem
  using ( module UnionKit; module HullStage; module HullElemDown )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prodL; ω⊆; Goal; module Step )
```

这条路线需要两种不同的控制。一个具有充分闭包性质的序数 `lam` 提供环境层，使壳与凝聚论证能在其中进行。编码单射则控制大小：先得到 `X ↪ κ`，再得到 `M ↪ κ`，最终得到 `β ↪ κ`。

```agda
open import L.GCH.AdequateStages {ℓ} lem using ( superadequate-above; Superadequate )
open import L.GCH.StageCountingTools {ℓ} lem using ( move )
open import L.GCH.StageInjection {ℓ} lem using ( stage-counted; module Site )
open import L.GCH.OmegaRecursion {ℓ} lem using ( pairʟ-in )
open import L.GCH.HullCounting {ℓ} lem
```

大小估计从两个简单部分开始。层 `Lset κ` 可以编码单射入 `κ`，单点集也可以编码单射入 `κ`。有限标签使两部分的像保持分离，而无穷内部基数 `κ` 的平方律把所得乘积重新吸收到 `κ` 中。

```agda
  using ( ord⊆Lset; module Union2; tag-union; module Point; module Count )
```

下文若干相等通过双向比较成员关系来证明。并集隶属给出的分支带有命题截断，但每个目标隶属陈述本身都是命题，因此可以局部使用这些分支，而不必选定并保留某个分支。

```agda
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
```

有限 von Neumann 数码提供并集编码所需的标签，序数后继闭包则是壳所需环境的一部分。良基性支撑平方律。命题截断记录编码单射的存在，却不暴露一张选定的图。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet; ⁅_⁆s )
open InfinitySet {ℓ} using ( #_; ω; sucV )
import Cubical.Induction.WellFounded as WF
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
```

凡是通过 `InjL` 断言单射时，其图都只在命题截断下存在。证明可以在命题内部复合这些存在性，却不会得到一条能在截断之外作为计算数据使用的指定单射。

```agda
open PT using ( ∣_∣₁ )
```

子集前提刻意用外围隶属来陈述。因此可以对任意外围集合 `z` 检验它属于 `y`，继而推出它属于 `κ`；并不要求 `z` 一开始就附带自身的可构造性证明。

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
```

与之相对，`κ` 与 `y` 是可构造载体 `S` 的元素：二者都把外围集合与其属于 `L` 的证据打包在一起。最终见证也以同样方式打包，因此定理给出的是可构造序数，而不是任意外围序数。

```agda
open hPropStructure 𝒮ʟ using ( S )
```

## 为基数的可构造子集取界

固定可构造集合 `κ`，假设其底层集合是序数、是内部基数且不属于 `ω`。再固定任意可构造集合 `y`，并逐点假设 `y` 的每个外围成员都属于 `κ`。这些就是全部前提；特别地，不假设 `y` 由公式或有限多个参数定义。

```agda
module At (κ : S) (oκ : IsOrd (fst κ)) (cκ : IsCardinalL κ)
          (κ∉ω : ⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
          (y : S) (y⊆κ : (z : V ℓ) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ fst κ ⟩) where
```

由 `κ` 的序数性与 `κ ∉ ω` 可得 `ω ⊆ κ`。每个有限 von Neumann 数码 `# k` 都属于 `ω`，所以对每个 `k` 都有 `# k ∈ κ`。这些元素将充当并集编码中的有限标签。

```agda
  num∈κ : (k : ℕ) → ⟨ # k ∈ fst κ ⟩
  num∈κ k = ω⊆ (fst κ) oκ κ∉ω (# k) (#∈ω k)
```

序数 `κ` 与以它为指标的可构造层是两个不同的集合。因此把 `Lset κ` 打包为内部集合 `Lκ`；该层将构成起始集的主要部分，而 `κ` 自身仍是起始集所要编码单射入的基数。

```agda
  Lκ : S
  Lκ = LsetS (fst κ) oκ
```

为了把 `κ` 与 `y` 放进同一个层，先在 `L` 内形成二者的无序对。任何包含该对的传递层都会包含它的两个成员，因此只需一次出现层构造便能同时处理这两个对象。

```agda
  private
    P₀ : S
    P₀ = pairʟ κ y
```

选取序数层索引 `α₀`，使该无序对出现在其所索引的层中。这只是由可构造性给出的一个方便的出现索引；这里没有断言 `α₀` 是该对最早出现的层。

```agda
    α₀ : V ℓ
    α₀ = stage (fst P₀) (snd P₀)
```

所选层索引 `α₀` 是序数。这一点很关键：下一步要取得严格高于它的超充分序数，稍后还要用序数的传递性把 `κ` 从 `α₀` 以下继续送入 `lam`。

```agda
    oα₀ : IsOrd α₀
    oα₀ = stage-ord (fst P₀) (snd P₀)
```

基数 `κ` 属于 `Lset α₀`。这是因为 `κ` 是无序对的成员，该无序对属于 `Lset α₀`，而这一层是传递集。这里得到的是层隶属，尚不是后文所用的序数隶属 `κ ∈ α₀`。

```agda
    κ∈Lα₀ : ⟨ fst κ ∈ˢ Lset α₀ ⟩
    κ∈Lα₀ = layer-trans (Lset-layer α₀) {x = fst P₀} {y = fst κ}
      (pairʟ-in κ y κ (inl refl)) (stage-mem (fst P₀) (snd P₀))
```

同一个传递性论证经无序对的另一成员把 `y` 放进 `Lset α₀`。与 `κ` 不同，并未假设 `y` 是序数，所以后文会用层的单调性把这一事实搬到 `Lset lam`，而不会把它转换成 `y ∈ α₀`。

```agda
    y∈Lα₀ : ⟨ fst y ∈ˢ Lset α₀ ⟩
    y∈Lα₀ = layer-trans (Lset-layer α₀) {x = fst P₀} {y = fst y}
      (pairʟ-in κ y y (inr refl)) (stage-mem (fst P₀) (snd P₀))
```

现在显式选取超充分序数 `lam`，满足 `α₀ ∈ lam`。这个严格扩张提供后续壳与凝聚论证所需的闭包性质。`lam` 自身虽是显式数据，但其超充分性所保证的局部充分指标仍处于命题截断下。

```agda
    sa = superadequate-above α₀ oα₀
```

把这个高序数在代码中记作 `lam`，正文中记作 `λ`。它的具体构造后文不再起作用；证明只使用其序数性、后继闭包、超充分性以及它高于 `α₀` 这一事实。

```agda
  opaque
    lam : V ℓ
    lam = sa .fst
```

首先保留的事实是 `lam` 为序数。因此它是传递集，这使得 `lam` 以下的序数隶属可以继续向上传递。

```agda
    ordλ : IsOrd lam
    ordλ = sa .snd .fst
```

其次保留对序数后继的闭包：只要 `d ∈ lam`，便有 `sucV d ∈ lam`。这项闭包是保证有限 Skolem 构造留在 `lam` 所索引层内的结构前提之一。

```agda
    succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩
    succλ = sa .snd .snd .snd .fst .snd .fst
```

超充分性表示：对每个 `d ∈ lam`，都仅仅存在充分序数 `γ`，满足 `d ∈ γ ∈ lam`。它在 `lam` 以下提供局部的充分空间，却不选取最小的 `γ`，也不选取这样一族 `γ`。

```agda
    sup : Superadequate lam
    sup = sa .snd .snd .snd .snd
```

基数 `κ` 属于序数索引 `lam`。由于 `κ` 与 `α₀` 都是序数，先由 `κ ∈ Lset α₀` 得到 `κ ∈ α₀`；再结合 `α₀ ∈ lam` 与序数 `lam` 的传递性，得到 `κ ∈ lam`。这个结论说的是属于索引 `lam`，而不是属于层 `Lset lam`。

```agda
    κ∈λ : ⟨ fst κ ∈ˢ lam ⟩
    κ∈λ = ordλ .fst (ord∈Lset→∈ α₀ oα₀ (fst κ) oκ κ∈Lα₀) (sa .snd .snd .fst)
```

对 `y`，所需结论则是它属于层 `Lset lam`。由 `α₀ ∈ lam`，层的单调性给出 `Lset α₀ ⊆ Lset lam`；把它用于先前的 `y ∈ Lset α₀`，便得到 `y ∈ Lset lam`。这里不需要假设 `y` 是序数。

```agda
    y∈Lλ : ⟨ fst y ∈ˢ Lset lam ⟩
    y∈Lλ = Lset-mono {α = lam} {β = α₀} (sa .snd .snd .fst) y∈Lα₀
```

`y` 的每个外围成员都属于 `Lset κ`。子集前提先把 `z ∈ y` 送到 `z ∈ κ`；由于 `κ` 是序数，这样的 `z` 本身也是序数，属于自己的后继层，再由累积性得到 `z ∈ Lset κ`。因此，`y ⊆ κ` 给出了使起始集成为传递集所需的层包含关系。

```agda
  y⊆Lκ : (z : V ℓ) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ Lset (fst κ) ⟩
  y⊆Lκ z hz = ord⊆Lset (fst κ) oκ z (y⊆κ z hz)
```

在 `Lset lam` 内形成起始集 `X = Lset κ ∪ {y}`。它包含 `y`，并且是传递集：来自 `Lset κ` 的元素仍留在这个传递层中；来自 `y` 的元素则由假设属于 `κ`，因而属于 `Lset κ`。这项传递性正是后文使塌缩固定 `y` 的原因。

```agda
  module UK = UnionKit (fst κ) lam (fst y) oκ ordλ κ∈λ y⊆Lκ y∈Lλ κ∉ω
    using ( X; X⊆Lλ; ∅∈λ; Lα∈X; x∈X; X-mem; sgl≡; Xtr )
```

下文用 `X` 表示这个由 `Lset κ` 扩张而成的传递集。需要保留的两项性质彼此配合：`y ∈ X` 保证壳包含待定位的集合，传递性则保证塌缩不会改变它。

```agda
  X : V ℓ
  X = UK.X
```

为了计数，在内部构造单点集 `{y}` 及其到 `κ` 的编码单射，其中使用标签 `0 ∈ κ`，再把它与 `Lκ` 作内部并。这样得到同一集合 `Lset κ ∪ {y}` 的编码呈现，其两个部分已经分别带有带标签并集论证所需的单射。

```agda
  module Pt = Point κ (num∈κ 0) y using ( Y; Y-out; Y-in; injL )
  module U = Union2 Lκ Pt.Y using ( D; out; in₁; in₂ )
```

把这个内部构造的并记作 `Xʟ`。它与 `X` 表示同一个数学并集，但其构造附带了证明它编码单射入 `κ` 所需的内部数据。

```agda
  Xʟ : S
  Xʟ = U.D
```

为了把 `Xʟ` 与 `X` 识别起来，双向比较二者的成员。正向中，属于内部编码并意味着在命题截断下分成两种情形：属于 `Lset κ`，或属于编码单点集；两种情形都推出属于 `X`。由于属于 `X` 是命题，这次消去是合法的。

```agda
  Xʟ-eq : fst Xʟ ≡ X
  Xʟ-eq = extensionalV {a = fst Xʟ} {b = X} (λ z → ⇔toPath (fwd z) (bwd z))
    where
    fwd : (z : V ℓ) → ⟨ z ∈ˢ fst Xʟ ⟩ → ⟨ z ∈ˢ X ⟩
    fwd z h = PT.rec (snd (z ∈ˢ X)) go (U.out zS h)
```

在层这一分支中，左侧包含把该成员放入 `X`。把 `z` 暂时打包为可构造集合是由 `L` 的传递性保证的：既然 `z` 属于可构造集合 `Xʟ`，它自身也可构造。

```agda
      where
      zS : S
      zS = z , isL-trans {x = fst Xʟ} {y = z} h (snd Xʟ)
      go : ⟨ z ∈ˢ Lset (fst κ) ⟩ ⊎ ⟨ z ∈ˢ fst Pt.Y ⟩ → ⟨ z ∈ˢ X ⟩
      go (inl hz) = UK.Lα∈X z hz
```

在单点分支中，编码成员等于已知属于 `X` 的 `y`。反向中，属于 `X` 同样只在命题截断下拆分为 `Lset κ` 一侧与单点一侧；目标「属于 `Xʟ`」是命题，因此第二次消去同样合法。

```agda
      go (inr hz) = subst (λ w → ⟨ w ∈ˢ X ⟩) (sym (Pt.Y-out zS hz)) UK.x∈X
    bwd : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ fst Xʟ ⟩
    bwd z h = PT.rec (snd (z ∈ˢ fst Xʟ)) go (UK.X-mem z h)
      where
      go : ⟨ z ∈ˢ Lset (fst κ) ⟩ ⊎ ⟨ z ∈ˢ ⁅ fst y ⁆s ⟩ → ⟨ z ∈ˢ fst Xʟ ⟩
```

反向的两个分支分别进入 `Xʟ` 的两个并项。`Lset κ` 的成员从左侧进入，其可构造性由该层继承；`{y}` 的成员先与 `y` 识别，再从编码单点集一侧进入。因此外延性给出 `fst Xʟ ≡ X`，而不保留任何一次截断的分支选择。

```agda
      go (inl hz) = U.in₁ (z , isL-trans {x = Lset (fst κ)} {y = z} hz (snd Lκ)) hz
      go (inr hz) = subst (λ w → ⟨ w ∈ˢ fst Xʟ ⟩) (sym (UK.sgl≡ z hz)) (U.in₂ y Pt.Y-in)
```

起始集合可构造，因为内部副本可构造且两副本底层集合相等。

```agda
  X-isL : ⟨ isL X ⟩
  X-isL = subst (λ w → ⟨ isL w ⟩) Xʟ-eq (snd Xʟ)
```

把 `X` 连同这份可构造性证明打包为 `XS : S`。它的底层外围集合仍恰好是 `X`；这项打包只提供 `InjL` 所要求的内部定义域。

```agda
  XS : S
  XS = X , X-isL
```

无穷基数平方律给出编码单射 `κ × κ ↪ κ` 的命题截断存在。它所需的前提正是开头固定的事实：`κ` 是序数、内部基数且不属于 `ω`。这里既不产生双射，也不产生一张选定的单射图。

```agda
  pairκ : InjL (prodL κ) κ
  pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ κ∉ω
```

两条分量单射输入带标签并的构造，得到编码单射 `Xʟ ↪ κ × κ`：标签 `#0` 与 `#1` 区分层部分和单点集部分。再与平方律给出的单射复合，得到 `Xʟ ↪ κ`；最后沿 `fst Xʟ ≡ X` 搬运定义域，把它换成可构造包装 `XS`。所得正是需要的编码单射 `X ↪ κ`，并且仍处于命题截断下。

```agda
  base : InjL XS κ
  base = move Xʟ XS κ κ Xʟ-eq refl
    (injl-trans Xʟ (prodL κ) κ
      (tag-union κ (num∈κ 0) (num∈κ 1) Lκ Pt.Y (stage-counted κ Lκ oκ κ∉ω refl) Pt.injL)
      pairκ)
```

令 `M` 为 `X` 在 `Lset lam` 内生成的 Skolem 壳。适用于这个壳的 Tarski-Vaught 定理表明，`M` 具有凝聚所需的初等性。整个传递集 `X` 就是起始集，因此这正是包含 `y`、且其塌缩稍后将固定 `y` 的同一个壳。

```agda
  elem = HullElemDown.elem lam ordλ X UK.X⊆Lλ UK.∅∈λ
```

壳计数定理把 `X ↪ κ` 依次传过 Skolem 闭包的有限阶段及这些阶段的并，得到编码单射 `M ↪ κ` 在命题截断下的存在性。于是，这个壳既具有应用凝聚所需的初等性，其大小又仍受 `κ` 控制。

```agda
  hull↪κ = Count.hull↪κ lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL κ oκ cκ κ∉ω base
```

凝聚给出显式序数 `β`，并把 `M` 的塌缩像识别为 `Lset β`。它还把 `Lset β` 与 `M` 打包为可构造集合，并通过逆塌缩给出编码单射 `Lset β ↪ M` 的命题截断存在。这里 `β` 是层索引，`Lset β` 才是它所索引的层。

```agda
  module St = Site lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL
    using ( β; oβ; ext; Lβ; βL; hullL; Lβ↪M )
```

下面使用同一个壳构造的三个方面：壳 `M`、包含关系 `X ⊆ M`，以及像为 `πX` 的塌缩映射 `π`。相应的不动点定理适用于 `M` 的传递子集。这些事实将先证明塌缩不改变 `y`，再把同一个 `y` 放入凝聚所识别出的层中。

```agda
  module HS = HullStage lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( X⊆M )
  module HSC = HullStage.C lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ
    using ( πX; π; fixes; πX-intro )
```

集合 `y` 属于 Skolem 壳 `M`：它已被放入起点集 `X`，而 `X` 的每个成员都属于由 `X` 生成的壳。

```agda
  y∈M : ⟨ fst y ∈ˢ HS.M ⟩
  y∈M = HSH.X⊆M (fst y) UK.x∈X
```

塌缩固定 `y`：因为起点集 `X` 传递且包含于壳中，塌缩映射在 `X` 的每个成员上恒等，而 `y` 即为其中之一。

```agda
  πy : HSC.π (fst y) ≡ fst y
  πy = HSC.fixes X
    (λ a a∈ₛX → ∈∈ₛ {a = a} {b = HS.M} .fst (HSH.X⊆M a (∈∈ₛ {a = a} {b = X} .snd a∈ₛX)))
    UK.Xtr (fst y) UK.x∈X
```

由于 `y` 属于壳，塌缩像包含 `π(y)`。凝聚把这个像认同为可构造层 `Lset β`，再由不动点等式 `π(y) = y` 得到 `y ∈ Lset β`。关键在于，塌缩没有用另一个集合替换 `y`，而是把原来的 `y` 定位在一个受控的可构造层中。

```agda
  y∈Lβ : ⟨ fst y ∈ˢ Lset St.β ⟩
  y∈Lβ = subst (λ w → ⟨ w ∈ˢ Lset St.β ⟩) πy
    (subst (λ w → ⟨ HSC.π (fst y) ∈ˢ w ⟩) St.ext (HSC.πX-intro (fst y) y∈M))
```

序数 `β` 经三条编码单射的链注入 `κ`：由序数隶属从 `β` 到层 `Lset β` 的包含、由受限逆塌缩从 `Lset β` 到壳 `M` 的单射、以及由壳计数从 `M` 到 `κ` 的单射。这条链给出的是编码单射，而非裸序数比较。

```agda
  β↪κ : InjL St.βL κ
  β↪κ = injl-trans St.βL St.Lβ κ
    (inclusion-coded St.βL St.Lβ (λ z hz → ord⊆Lset St.β St.oβ z hz))
    (injl-trans St.Lβ St.hullL κ St.Lβ↪M hull↪κ)
```

局部见证现把可构造序数 `β`、它的序数性、`y` 属于层 `Lset β` 的事实，以及编码单射 `β ↪ κ` 打包在一起。这里返回的是层指标 `β`，而 `Lset β` 是已经容纳 `y` 的可构造层；二者不可混同。

```agda
  result : Σ[ b ∈ S ] (IsOrd (fst b) × ⟨ fst y ∈ˢ Lset (fst b) ⟩ × InjL b κ)
  result = St.βL , St.oβ , y∈Lβ , β↪κ
```

最后，`∣_∣₁` 把整个局部见证置于命题截断下。因此，最终定理只保留如下存在性：某个可构造序数 `β` 满足 `y ∈ Lset β`，并存在编码单射 `β ↪ κ`。它既不提供最小或规范的 `β`，也不随 `y` 统一选取见证。

```agda
internal-bounded-subset : InternalBoundedSubset
internal-bounded-subset κ oκ cκ κ∉ω y y⊆κ =
  ∣ At.result κ oκ cκ κ∉ω y y⊆κ ∣₁
```