Let α be given.

Assume Ha: ordinal α.

Let x be given.

Assume H1: x ∈ SNoS_ α.

We will prove ∃β ∈ α, SNo_ β x.

An exact proof term for the current goal is SepE2 (𝒫 (SNoElts_ α)) (λx ⇒ ∃β ∈ α, SNo_ β x) x H1.

∎