We are at last ready to construct R as a Σsplit subspace of the bounded interval predomain IR, and hence of Σ^{Q}×Σ^{Q}.
Remark 8.1 Because of Lemma 5.11,
the process of defining R by means of a nucleus E on IR,
where IR is in turn defined by a nucleus E_{1} on Σ^{Q}×Σ^{Q},
is the same as giving a nucleus E on the larger space for which
E·E_{1} = E = E·E = E_{1}· E. 
Naturally, it will simplify the proof if we can restrict attention to (δ,υ):IR, i.e. pseudocuts that are rounded, bounded and disjoint, thereby isolating locatedness.
However, another reason for considering R as a subspace of IR is that E then becomes a nucleus in the sense of both ASD and locale theory (Definition 5.5). The latter says that id⊑E=E^{2} and it preserves meets, so we have to prove that
Φ(δ,υ) ⇔ E_{1}Φ(δ,υ) ⇒ EΦ(δ,υ) and EΦ(δ,υ) ∧ EΨ(δ,υ) ⇒ E(Φ∧Ψ)(δ,υ), 
on the assumption that (δ,υ):IR. (Only the last of these actually remains to be done.) We use Proposition 7.10 to eliminate this hypothesis, by applying E_{1}. In Proposition 8.9 we shall deduce the equations in Lemma 5.4 from these results.
Notation 8.2 As the formula in Proposition 2.17
only involves variables ranging over Q, Σ^{Q}
and Σ^{ΣQ×ΣQ}, we may import it into the logic of ASD.
However, we prefer to use
E Φ(δ,υ) ≡ ∃ n≥ 1. ∃ q_{0}<⋯< q_{n}. 
 q_{0}∧ 
 q_{n} ∧ ⋀_{k=0}^{n−1} Φ(δ_{qk}, υ_{qk+1}), 
with δ and υ instead of δ and υ, and no n≡0 term (which would be ∇). The reason is the same as for the choice of E_{1} in preference to E_{1}′ or E_{rdb}, namely that it commutes with E_{r} and preserves ⊥ (Exercises 7.15f). Propositions 2.15 and 2.17 could be adapted to this choice by replacing I there with
I V ≡ {(D,U) ∣ ∃ d e u t.d< e∧ e∈ D∧[d,u]⊂ V∧ t∈ U∧ t< u}. 
We have already said in Remark 6.15 that equality on Q must be decidable in order to use ASD’s methods of “discrete mathematics”. In particular, note that “∃ q_{0}<⋯< q_{n}” is existential quantification over List (Q), not just n+1fold quantification over Q.
Notice that E_{1} is the n≡ 1 disjunct of E, so E_{1}⊑E.
We begin with some lemmas for managing the sequence.
Lemma 8.3 For any (δ,υ),
suppose EΦ(δ,υ) holds by virtue of the sequence
q_{0}<⋯< q_{n}, and that q_{0}≤ r≤ q_{n}.
Then EΦ(δ,υ) also holds by virtue of the sequence
obtained by inserting r.
Proof If q_{k} < r < q_{k+1} then Φ(δ_{qk}, υ_{qk+1}) ⇒ Φ(δ_{qk}, υ_{r}) ∧ Φ(δ_{r}, υ_{qk+1}). ▫
Lemma 8.4 For any Φ,
and understanding that q_{0}≡ d and q_{n}≡ u, the predicate
θ(d,u)≡∃ d< q_{1}<⋯< q_{n−1}< u. ⋀_{k=0}^{n−1}Φ(δ_{qk},υ_{qk+1}) 
is rounded, in the sense that θ(e,t) ⇔ ∃ d u.(d< e)∧(t< u)∧θ(d,u) =⇒ e< t.
Proof First, θ(d,u)⇒ d< u because there are d< q_{1}<⋯< q_{n−1}< u.
[⇐] If θ(d,u) holds by virtue of some sequence d=q_{0}<⋯< q_{n}=u, and d< e< t< u, then the same sequence with e and t in place of q_{0} and q_{n}, but omitting any q_{i}< e or > u, justifies θ(e,t).
[⇒] By Lemma 8.3, we may assume that n≥ 3 in the expansion of θ. The idea is to separate the left and rightmost conjuncts from the rest, and then enlarge them using Proposition 7.12:

This was the condition in Proposition 7.13 for θ to extend from intervals with rational endpoints to more general rounded, bounded and disjoint ones:
EΦ(δ_{d},υ_{u}) ⇔ ∃ d< q_{1}⋯< q_{n−1}< u. ⋀_{k=0}^{n−1} Φ(δ_{qk},υ_{qk+1}). 
Although θ(d,u)⇔⊥ when d≥ u, we shall see in Propositions 8.12 and 10.5 that, in this case,
EΦ(δ_{x},υ_{x}) ⇔ Φ(δ_{x},υ_{x}) and EΦ(δ_{d},υ_{u}) ⇔ ∃ x:[u,d].Φ(δ_{x},υ_{x}). 
Proof The expansion of EΦ(δ_{d},υ_{u}) involves δ_{d} q_{0}∧υ_{u} q_{n}≡(q_{0}< d< u< q_{n}). So, by Lemma 8.3, we may assume that d and u occur in the given sequence, say as d≡ q_{i}, u≡ q_{j}. But then q_{0},…,q_{i−2} and q_{j+2},…, q_{n} are redundant, so without loss of generality d≡ q_{1} and u≡ q_{n−1}. Hence by Lemma 8.4,
EΦ(δ_{d},υ_{u}) ⇔ ∃ q_{0}< d< u< q_{n}.θ(q_{0},q_{n}) ⇔ θ(d,u). ▫ 
We can now carry out the plan in Remark 8.1. The first two results say that the subspace R that will be defined by E is contained in that defined by E_{1}, which is IR. Notice that the expansion of E_{1}·E in the second result inherits the δ and υ from E_{1}, so they must also be used in the definition of E in order to obtain the equation E_{1}·E=E.
Lemma 8.6 E(E_{1}Φ)(δ,υ) ⇔ EΦ(δ,υ)
and E_{1}(EΦ)(δ,υ) ⇔ EΦ(δ,υ).
Proof The first part involves the conjuncts E_{1}Φ(δ_{qk},υ_{qk+1}) that occur in the expansion of the formula for E(E_{1}Φ)(δ,υ). Such (δ_{qk},υ_{qk+1}) are rounded, bounded and disjoint, so
E_{1}Φ(δ_{qk},υ_{qk+1}) ⇔ Φ(δ_{qk},υ_{qk+1}) 
by Proposition 7.12. These are the same conjuncts that are used in the expansion of EΦ(δ,υ).
In the second part, using Lemma 8.5,

Lemma 8.7 E^{2}Φ(δ,υ)=⇒EΦ(δ,υ).
Proof The outer E of E^{2} involves a sequence q_{0}<⋯< q_{n} and conjuncts EΦ(δ_{qk},υ_{qk+1}) for each 0≤ k≤ n−1. By Lemma 8.5, the expansion of each of these involves a sequence
q_{k} = r_{k,0}<⋯< r_{k,mk} = q_{k+1} 
with conjuncts Φ(δ_{rk,j},υ_{rk,j+1}). All of these sequences can be concatenated, to yield one that justifies EΦ(δ,υ). ▫
The final preparatory result is the one that says that E is a nucleus on IR in the sense of locale theory, as well as that of ASD.
Proposition 8.8
If (δ,υ) are rounded, bounded and disjoint then
E⊤(δ,υ) ⇔ ⊤ and EΦ(δ,υ) ∧ EΨ(δ,υ) =⇒ E(Φ∧Ψ)(δ,υ). 
Proof As (δ,υ) are rounded and bounded, ⊤⇔E_{1}⊤(δ,υ)⇒E⊤(δ,υ) by Lemma 7.7.
Suppose that EΦ and EΨ are justified by sequences q_{0}<⋯< q_{n} and r_{0}<⋯< r_{m} respectively. Let
d ≡ max(q_{0},r_{0}) and u≡ min(q_{n},r_{m}), 
so d is either q_{0} or r_{0}, which both satisfy δ, so δ d holds, as similarly does υ u. Since (δ,υ) are rounded and disjoint, d< u by Lemma 7.5. Now let
d ≡ s_{0}< ⋯ < s_{ℓ} ≡ u 
be the union of the given sequences q_{0}<⋯< q_{n} and r_{0}<⋯< r_{m}, removing duplicates and those terms < d or > u. Such outlying points were already redundant in the expansion of EΦ(δ,υ) and of EΨ(δ,υ), whilst by Lemma 8.3 we may adjoin the members of one sequence to the other. Hence the new combined sequence serves for both EΦ(δ,υ) and EΨ(δ,υ), and therefore for E(Φ∧Ψ)(δ,υ) too. ▫
Proposition 8.9
E is a nucleus (Definition 5.5), as it satisfies,
for Φ,Ψ:Σ^{ΣQ×ΣQ},
E(Φ∧ Ψ) = E(E Φ∧E Ψ) and E(Φ∨ Ψ) = E(E Φ∨E Ψ). 
Proof For (δ,υ):IR, Proposition 7.12 gives Φ(δ,υ)⇔ E_{1}Φ(δ,υ) ⇒ EΦ(δ,υ), so
(Φ∧Ψ)(δ,υ) ⇒ (EΦ∧EΨ)(δ,υ) (Φ∨Ψ)(δ,υ) ⇒ (EΦ∨EΨ)(δ,υ) 
and
EΦ(δ,υ)∨EΨ(δ,υ) ⇒ E(Φ∨Ψ)(δ,υ), 
whilst
EΦ(δ,υ)∧EΨ(δ,υ) ⇒ E(Φ∧Ψ)(δ,υ) 
by Proposition 8.8. Then we use Proposition 7.10 to eliminate the hypothesis (δ,υ):IR, and obtain the first inequality in each row:

The second inequality follows from E_{1}⊑E, and the third, E^{2}⊑E, is Lemma 8.7. Finally, from each E_{1}Θ⊑EΩ, we deduce EΘ=E(E_{1}Θ)⊑E^{2}Ω⊑EΩ by Lemmas 8.6 and 8.7. ▫
This fulfils the obligation that we have before invoking the ASD technology in Section 5, so we can now introduce the type R≡{Σ^{ΣQ×ΣQ} ∣ E}. We still have to characterise its admissible terms, i.e. to show that the equalisers in Remarks 5.2 and 6.9 are isomorphic.
The following is the main lemma to do this. In it, (δ,υ) need not be disjoint, so it may represent a backtofront interval like those in Remark 2.20, which we shall use to compute existential quantifiers. In the proof, we have to switch back from using abutting closed intervals to overlapping open ones, cf. the proof of Proposition 2.17.
Lemma 8.10
If (δ,υ) is located
then EΦ(δ,υ) ⇔ E_{1}Φ(δ,υ).
Proof [⇐] is trivial. For [⇒], we use Proposition 7.12 to widen the argument of each conjunct Φ a little towards the right, from [q_{k},q_{k+1}] to [q_{k},r_{k+1}], for any q_{k+1}< r_{k+1}< q_{k+2}:

where υ q_{n}⇒υ r_{n} because υ is upper. As (δ,υ) is located with δ q_{0} and υ r_{n}, we may apply Lemma 6.16 to this sequence. Because of the alternation of letters, it gives
⋁_{k=0}^{n−1}( 
 q_{k}∧ 
 q_{k+1}) ∨ ⋁_{k=0}^{n−1}( 
 r_{k}∧ 
 r_{k+1}). 
We already have the corresponding Φ(δ_{qk},υ_{qk+1}) from the original abutting expansion, whilst the one with overlapping intervals provides
Φ(δ_{qk},υ_{rk+1}) =⇒ Φ(δ_{rk},υ_{rk+1}), 
since δ_{qk}⊑δ_{rk}. Hence, with e≡ q_{k}< t≡ q_{k+1} or e≡ r_{k}< t≡ r_{k+1}, we have
EΦ(δ,υ) =⇒ ∃ e< t. 
 e∧ 
 t∧ Φ(δ_{e},υ_{t}) ≡ E_{1}Φ(δ,υ). ▫ 
Lemma 8.11
If (δ,υ) is rounded and bounded,
and EΦ(δ,υ)=⇒E_{1}Φ(δ,υ)
for all Φ, then (δ,υ) is located.
Proof For any d< u, there is a sequence of rationals
q_{0}< d< q_{1}< u< q_{2} with δ q_{0} and υ q_{2}. 
These numbers satisfy δ_{q0}d⇔⊥, υ_{q1}u⇔⊤, δ_{q1}d⇔⊤ and υ_{q2}u⇔⊥, so
∃ q_{0}< q_{1}< q_{2}. δ q_{0} ∧ υ q_{2} ∧ (δ_{q0}d∨υ_{q1}u) ∧ (δ_{q1}d∨υ_{q2}u). 
This is the n≡ 2 disjunct of EΦ(δ,υ), where Φ(α,β)≡α d∨β u. By hypothesis, this implies E_{1}Φ(δ,υ), where

Proposition 8.12
(δ,υ) is a cut iff it is admissible for E.
Proof If it’s a cut then in particular it’s rounded, bounded and disjoint, so Φ(δ,υ)⇔E_{1}Φ(δ,υ) by Proposition 7.12. As it’s also located, EΦ(δ,υ)⇔E_{1}Φ(δ,υ) by Lemma 8.10, so (δ,υ) is admissible.
Conversely, admissibility of (δ,υ) for E with respect to both Φ and E_{1}Φ, give
Φ(δ,υ) ⇔ EΦ(δ,υ) ⇔ E(E_{1}Φ)(δ,υ) ⇔ E_{1}Φ(δ,υ), 
where the middle implication is Lemma 8.6. Hence (δ,υ) is also admissible for E_{1}, so it is rounded, bounded and disjoint by Theorem 7.14. It is also located, by Lemma 8.11. ▫
Theorem 8.13 The type R≡{Σ^{ΣQ×ΣQ} ∣ E} is
the equaliser in Remark 6.9, i.e. its terms are Dedekind
cuts, and the inclusion R↣Σ^{ΣQ×ΣQ} is Σsplit. ▫
In the following two sections, we shall show that this construction does make the real line Dedekindcomplete and the closed interval compact.