---
title: "Bounded subsets appear at controlled stages"
module: L.GCH.BoundedSubset
lang: en
site: "Bedrock"
description: "Bounded subsets appear at controlled stages"
stage: "Proving GCH"
reading_order: 119
canonical: https://bedrock.institute/en/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/zh/L.GCH.BoundedSubset.md, https://bedrock.institute/ja/L.GCH.BoundedSubset.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Bounded subsets appear at controlled stages

The bounded-subset theorem starts with an internal cardinal `κ` whose underlying set is an ordinal and does not belong to `ω`, together with an arbitrary constructible set `y` whose ambient members all lie in `κ`. Under propositional truncation, it gives a constructible ordinal `β` such that `y ∈ Lset β` and a coded injection `β ↪ κ` exists. It assumes no formula defining `y`, selects no least stage, and makes no uniform choice of `β` as `y` varies.

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

The proof is classical only through the displayed instance of excluded middle. This hypothesis supports the earlier constructions of stages, hulls, and coded maps used here; it does not turn the final truncated existence into a chosen family of witnesses.

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

Fix a universe level `ℓ` and excluded middle at level `ℓ-suc ℓ`. Every construction below, including the final bounded-subset theorem, depends on this single classical hypothesis and on no choice principle.

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

Two levels of objects must be kept separate throughout the argument. Symbols such as `κ`, `α₀`, `lam`, and later `β` denote sets in the ambient cumulative hierarchy, some proved to be ordinals; `Lset κ`, `Lset α₀`, `Lset lam`, and `Lset β` denote the corresponding constructible stages. Membership in a stage index and membership in its indexed stage are different assertions.

```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 ( #∈ω )
```

The first task is to place both `κ` and `y` in one sufficiently high constructible stage. Since `y` is already supplied as a constructible set, an occurrence stage can be obtained directly; no formula defining `y`, and no finite list of defining parameters, enters this construction.

```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 )
```

The central strategy is to enlarge `Lset κ` by the single point `y`, generate an elementary Skolem hull from that transitive starting set, and apply condensation. Counting the starting set by `κ` will count the whole hull by `κ`; condensation will then convert the collapsed hull into a stage `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 )
```

This plan needs two different kinds of control. A sufficiently closed ordinal `lam` provides the ambient stage in which the hull and condensation argument can be carried out. Coded injections control size: first `X ↪ κ`, then `M ↪ κ`, and finally `β ↪ κ`.

```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
```

The size estimate begins with two elementary pieces. The stage `Lset κ` can be coded into `κ`, and a singleton can also be coded into `κ`. Finite tags keep their images disjoint, while the square law for the infinite internal cardinal `κ` absorbs the resulting product back into `κ`.

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

Several equalities below are proved by comparing membership in both directions. The alternatives arising from union membership are propositionally truncated, but each target membership statement is a proposition, so those alternatives may be used locally without selecting a lasting branch.

```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 ( ∈∈ₛ )
```

Finite von Neumann numerals provide the tags used in the union coding, while ordinal successor closure is part of the environment needed for the hull. Well-foundedness supports the square law. Propositional truncation records the existence of coded injections without exposing a chosen graph.

```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
```

Whenever an injection is asserted through `InjL`, its graph exists only under propositional truncation. The proof may compose such existences inside propositions, but it never obtains a distinguished injection that can be used as computational data outside the truncation.

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

The subset premise is deliberately stated with ambient membership. Thus an arbitrary ambient set `z` may be tested for membership in `y` and then in `κ`; `z` is not required to arrive together with its own proof of constructibility.

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

By contrast, `κ` and `y` are elements of the constructible carrier `S`: each packages an ambient set with evidence that it belongs to `L`. The eventual witness is packaged in the same way, so the theorem produces a constructible ordinal rather than an arbitrary ambient ordinal.

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

## Bounding a constructible subset of a cardinal

Fix a constructible set `κ` whose underlying set is an ordinal, an internal cardinal, and not a member of `ω`. Also fix an arbitrary constructible set `y` and assume pointwise that every ambient member of `y` belongs to `κ`. These are the complete hypotheses: in particular, no definition of `y` by a formula or by finitely many parameters is assumed.

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

The assumptions that `κ` is an ordinal and `κ ∉ ω` imply `ω ⊆ κ`. Since every finite von Neumann numeral `# k` belongs to `ω`, it follows that `# k ∈ κ` for every `k`. These elements will serve as the finite tags in the union coding.

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

The ordinal `κ` and the constructible stage indexed by it are different sets. We therefore package `Lset κ` as the internal set `Lκ`; this stage will form the large part of the starting set, while `κ` itself remains the cardinal into which that starting set is coded.

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

To place `κ` and `y` in one common stage, first form their unordered pair inside `L`. A stage containing this pair will contain both entries by transitivity, so one occurrence-stage construction suffices for the two objects.

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

Choose an ordinal stage index `α₀` at whose stage the pair occurs. This is a convenient occurrence index supplied by constructibility; nothing here says that `α₀` is the least stage at which the pair appears.

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

The chosen stage index `α₀` is an ordinal. This matters because the next construction asks for a superadequate ordinal strictly above it and because ordinal transitivity will later carry `κ` from below `α₀` into `lam`.

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

The cardinal `κ` belongs to `Lset α₀`. Indeed, `κ` is a member of the unordered pair, the pair belongs to `Lset α₀`, and this stage is transitive. This is stage membership, not yet the ordinal membership `κ ∈ α₀` used later.

```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₀))
```

The same transitivity argument places `y` in `Lset α₀` through the other member of the pair. Unlike `κ`, the set `y` is not assumed to be an ordinal, so this fact will be transported to `Lset lam` by stage monotonicity rather than converted into membership in `α₀`.

```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₀))
```

Now choose explicitly a superadequate ordinal `lam` with `α₀ ∈ lam`. This strict extension provides enough closure for the later hull and condensation arguments. Although `lam` itself is explicit, the adequate subindices promised by its superadequacy remain under propositional truncation.

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

Write this high ordinal as `lam`, corresponding to `λ` in the exposition. Its particular construction will play no further role; the proof uses its ordinality, successor closure, superadequacy, and its position above `α₀`.

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

The first retained fact is that `lam` is an ordinal. Consequently it is transitive, which will allow ordinal memberships below `lam` to be carried farther upward.

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

The second retained fact is closure under ordinal successor: whenever `d ∈ lam`, also `sucV d ∈ lam`. This closure is one of the structural hypotheses under which the finite Skolem construction remains inside the stage indexed by `lam`.

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

Superadequacy says that for each `d ∈ lam` there merely exists an adequate ordinal `γ` with `d ∈ γ ∈ lam`. It supplies local adequate room below `lam` without choosing a least `γ` or a family of such choices.

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

The cardinal `κ` belongs to the ordinal index `lam`. Because both `κ` and `α₀` are ordinals, `κ ∈ Lset α₀` first yields `κ ∈ α₀`. The relation `α₀ ∈ lam` and the transitivity of the ordinal `lam` then give `κ ∈ lam`. This conclusion concerns the index `lam`, rather than the stage `Lset lam`.

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

For `y`, the required conclusion is instead membership in the stage `Lset lam`. Since `α₀ ∈ lam`, monotonicity gives `Lset α₀ ⊆ Lset lam`; applying it to the earlier fact `y ∈ Lset α₀` yields `y ∈ Lset lam`. No ordinality of `y` is needed.

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

Every ambient member of `y` lies in `Lset κ`. Indeed, the subset hypothesis sends `z ∈ y` to `z ∈ κ`; since `κ` is an ordinal, such a `z` is itself an ordinal, lies in its successor stage, and hence lies in `Lset κ` by cumulativity. Thus `y ⊆ κ` supplies the stage inclusion needed to make the starting set transitive.

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

Form the starting set `X = Lset κ ∪ {y}` inside `Lset lam`. It contains `y` and is transitive: elements inherited from `Lset κ` stay in that transitive stage, while an element of `y` lies in `κ` by hypothesis and hence in `Lset κ`. This transitivity is precisely what will make the collapse fix `y` later.

```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 )
```

From now on, `X` denotes this transitive enlargement of `Lset κ`. The two features to retain are complementary: `y ∈ X` ensures that the hull contains the set we want to locate, and transitivity ensures that the collapse does not alter it.

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

For counting, construct the singleton `{y}` internally together with its injection into `κ`, using the tag `0 ∈ κ`, and take its internal union with `Lκ`. This produces a coded presentation of the same set `Lset κ ∪ {y}` whose two pieces already carry the injections needed for the tagged-union argument.

```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₂ )
```

Call this internally constructed union `Xʟ`. It represents the same mathematical union as `X`, but its construction carries the internal coding data needed to prove an injection into `κ`.

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

To identify `Xʟ` with `X`, compare their members in both directions. In the forward direction, membership in the internally coded union yields, under propositional truncation, either a member of `Lset κ` or a member of the coded singleton; both cases imply membership in `X`. The elimination is valid because membership in `X` is a proposition.

```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)
```

In the stage case, the left inclusion places the member in `X`. The temporary packaging of `z` as constructible is justified by transitivity of `L`: since `z` belongs to the constructible set `Xʟ`, it is constructible as well.

```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
```

In the singleton case, the coded member is equal to `y`, already known to belong to `X`. Conversely, membership in `X` splits, again only under propositional truncation, into the `Lset κ` side and the singleton side; the target membership in `Xʟ` is a proposition, so this second elimination is equally legitimate.

```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ʟ ⟩
```

The reverse cases enter the two summands of `Xʟ`. A member of `Lset κ` enters on the left, with constructibility inherited from that stage; a member of `{y}` is first identified with `y` and then enters through the coded singleton. Thus extensionality proves `fst Xʟ ≡ X` without retaining either truncated case split.

```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)
```

The starting set is constructible, since the internal copy is constructible and the two copies have equal underlying sets.

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

Package `X` together with this constructibility proof as `XS : S`. Its underlying ambient set is still exactly `X`; the packaging merely supplies the internal domain required by `InjL`.

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

The infinite-cardinal square law gives the propositionally truncated existence of a coded injection `κ × κ ↪ κ`. Its hypotheses are exactly the facts fixed at the start: `κ` is an ordinal internal cardinal and is not a member of `ω`. No bijection or chosen injection graph is produced.

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

The two component injections feed the tagged-union construction, giving a coded injection `Xʟ ↪ κ × κ`: tags `#0` and `#1` distinguish the stage part from the singleton part. Composing with the square-law injection gives `Xʟ ↪ κ`, and transport along `fst Xʟ ≡ X` changes the domain to the constructible package `XS`. The result is the required coded injection `X ↪ κ`, still under propositional truncation.

```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κ)
```

Let `M` be the Skolem hull generated by `X` inside `Lset lam`. The Tarski-Vaught theorem for this hull shows that `M` is elementary in the sense required by condensation. The whole transitive set `X` is the starting set, so this is the same hull that contains `y` and whose collapse will later fix `y`.

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

The hull-counting theorem propagates `X ↪ κ` through the finite stages of Skolem closure and then through their union. It yields the existence, under propositional truncation, of a coded injection `M ↪ κ`. The hull is therefore both elementary enough for condensation and small enough to remain controlled by `κ`.

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

Condensation supplies an explicit ordinal `β` and identifies the collapse image of `M` with `Lset β`. It also packages `Lset β` and `M` as constructible sets and gives the propositionally truncated coded injection `Lset β ↪ M` induced by the inverse collapse. Here `β` is the stage index, while `Lset β` is the stage it indexes.

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

We now use three aspects of this single hull construction: the hull `M`, the inclusion `X ⊆ M`, and the collapse map `π` with image `πX`. The associated fixed-point theorem applies to transitive subsets of `M`. These facts will first show that `y` is unchanged by the collapse and then place that same `y` in the stage identified by condensation.

```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 )
```

The set `y` belongs to the Skolem hull `M`: it was placed in the starting set `X`, and every member of `X` lies in the hull generated from `X`.

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

The collapse fixes `y`: because the starting set `X` is transitive and contained in the hull, the collapse map acts as the identity on every member of `X`, and `y` is one of them.

```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
```

The collapse image contains `π(y)`, since `y` belongs to the hull. Condensation identifies that image with the constructible stage `Lset β`, and the fixed-point equation `π(y) = y` then gives `y ∈ Lset β`. The point is that the collapse has not replaced `y` by another set: it has located the original `y` inside a controlled constructible stage.

```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))
```

The ordinal `β` injects into `κ` by a chain of three coded injections: the inclusion from `β` into the level `Lset β` by ordinal membership, the restricted inverse collapse from `Lset β` into the hull `M`, and the hull counting from `M` into `κ`. The chain gives a coded injection, not a bare ordinal comparison.

```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↪κ)
```

The local witness now packages the constructible ordinal `β`, its ordinality, the fact that `y` belongs to the stage `Lset β`, and the coded injection `β ↪ κ`. Here `β` is the stage index being returned, whereas `Lset β` is the constructible stage in which `y` has been located.

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

Finally, `∣_∣₁` places the entire local witness under propositional truncation. The final theorem therefore retains only that some constructible ordinal `β` satisfies `y ∈ Lset β` and admits a coded injection `β ↪ κ`. It provides neither a least nor a canonical `β`, and it makes no uniform choice of witnesses as `y` varies.

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