Let alpha be given.

Assume Ha: ordinal alpha.

Let x be given.

Assume H1: x ∈ SNoS_ alpha.

We will prove ∃beta ∈ alpha, SNo_ beta x.

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

∎