Let x be given.
Assume Hx H1 H2 H3.
We will prove x ∈ {x ∈ SNoS_ (ordsucc ω)|x ≠ ω ∧ x ≠ - ω ∧ (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x)}.
Apply SepI to the current goal.
An exact proof term for the current goal is Hx.
We will prove x ≠ ω ∧ x ≠ - ω ∧ (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x).
Apply and3I to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H3.
∎